diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:59:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:59:53 +0100 |
| commit | 563ee7cf230b85e7ed83c5652392f102974f662c (patch) | |
| tree | 2304cabcc02c9c3d6c1e055d3056f7b6e603e0aa /src/translation/HTLgenproof.v | |
| parent | 3ec28d050aebc305c6df5b4b95bcf91498ff11cc (diff) | |
| parent | f38fbe6e56bdf69cb5892b5397366ec3d0db9073 (diff) | |
| download | vericert-563ee7cf230b85e7ed83c5652392f102974f662c.tar.gz vericert-563ee7cf230b85e7ed83c5652392f102974f662c.zip | |
Merge branch 'master' into develop
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index be7538c..60f0d73 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -258,7 +258,7 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. +(* Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. Lemma symbols_preserved: @@ -1013,16 +1013,16 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. - Hint Resolve transl_final_states : htlproof. + Hint Resolve transl_final_states : htlproof.*) Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. - eapply Smallstep.forward_simulation_plus. +(* eapply Smallstep.forward_simulation_plus. apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. - exact transl_step_correct. -Qed. + exact transl_step_correct.*) +Admitted. End CORRECTNESS. |