diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 10:05:18 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 10:05:18 +0100 |
commit | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (patch) | |
tree | 1d4542a2b371d9e1d158a9ccfcade58b28cc9774 /cparser/StructReturn.ml | |
parent | d594c5da5e11fb10775c2b772961b8a2383887c7 (diff) | |
download | compcert-f00b70b6a17fdfb4e8606df891f6becc8102ef12.tar.gz compcert-f00b70b6a17fdfb4e8606df891f6becc8102ef12.zip |
Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.
Instead of assuming name uniqueness for all definitions in the program,
these variants only assume uniqueness for a particular name.
Use this approach to weaken the hypotheses for match_program
and transf_program_partial_augment.
Diffstat (limited to 'cparser/StructReturn.ml')
0 files changed, 0 insertions, 0 deletions