diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:31:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:31:03 +0100 |
| commit | 40a95b24099f9d70af32b14a4c79429ba03007f2 (patch) | |
| tree | 7d49cd7023850976e2736e7ad628ad694e5c9284 /src/translation/HTLgenproof.v | |
| parent | 5ca10a134176352b25a0b434d5508852c7314670 (diff) | |
| parent | 8486b4c046914b1388b68fe906fe267108f84267 (diff) | |
| download | vericert-kvx-40a95b24099f9d70af32b14a4c79429ba03007f2.tar.gz vericert-kvx-40a95b24099f9d70af32b14a4c79429ba03007f2.zip | |
Merge branch 'develop' into dev-nadesh-provendev-nadesh-proven
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 813a94b..943b76e 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -342,6 +342,7 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. + (* Lemma TRANSL' : *) (* Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. *) (* Proof. intros; apply match_prog_matches; assumption. Qed. *) |