diff options
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. *) |