From 01f42ef55d91bbb57b47ecc2be7e691165778980 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:38:06 +0200 Subject: fix Compiler.v --- backend/LICMproof.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'backend/LICMproof.v') diff --git a/backend/LICMproof.v b/backend/LICMproof.v index 065a7f74..2b76b668 100644 --- a/backend/LICMproof.v +++ b/backend/LICMproof.v @@ -12,6 +12,12 @@ Section PRESERVATION. Variables prog tprog: program. Hypothesis TRANSF: match_prog prog tprog. + Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. + Proof. + intros. eapply match_transform_partial_program_contextual; eauto. + Qed. + Theorem transf_program_correct : Smallstep.forward_simulation (semantics prog) (semantics tprog). Proof. -- cgit