diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 15:38:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 15:38:06 +0200 |
| commit | 01f42ef55d91bbb57b47ecc2be7e691165778980 (patch) | |
| tree | 401745d17f7d49800411de23826a3a975f4a3873 /backend/LICMproof.v | |
| parent | a3d40b88608b8b5e7e615346ea1c33198355cbbc (diff) | |
| download | compcert-kvx-01f42ef55d91bbb57b47ecc2be7e691165778980.tar.gz compcert-kvx-01f42ef55d91bbb57b47ecc2be7e691165778980.zip | |
fix Compiler.v
Diffstat (limited to 'backend/LICMproof.v')
| -rw-r--r-- | backend/LICMproof.v | 6 |
1 files changed, 6 insertions, 0 deletions
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. |