From f38fbe6e56bdf69cb5892b5397366ec3d0db9073 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 12:15:53 +0100 Subject: Admit everything temporarily --- src/translation/HTLgenproof.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 4b7f268..9786d23 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -205,7 +205,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: @@ -574,16 +574,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. -- cgit