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/Machine.ml | |
| parent | d594c5da5e11fb10775c2b772961b8a2383887c7 (diff) | |
| download | compcert-kvx-f00b70b6a17fdfb4e8606df891f6becc8102ef12.tar.gz compcert-kvx-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/Machine.ml')
0 files changed, 0 insertions, 0 deletions