diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-05 11:40:07 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
| commit | 3a244908dd9233100075ffe889b3da493cdf9c38 (patch) | |
| tree | 8c0a40b71d66729e07a52482ead28a0f45c2e59b /mppa_k1c/Machblockgenproof.v | |
| parent | 1412a262c0bb95ebc78ac7c4d79e0fa81954c82a (diff) | |
| download | compcert-kvx-3a244908dd9233100075ffe889b3da493cdf9c38.tar.gz compcert-kvx-3a244908dd9233100075ffe889b3da493cdf9c38.zip | |
Remplacement de match_prog par un plus classique
Diffstat (limited to 'mppa_k1c/Machblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Machblockgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index ff9c29d3..45ea53cc 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -23,9 +23,9 @@ Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.func Definition match_prog (p: Mach.program) (tp: Machblock.program) := match_program (fun _ f tf => tf = trans_fundef f) eq p tp. -Lemma transf_program_match: forall p, match_prog p (transf_program p). +Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp. Proof. - intros. eapply match_transform_program; eauto. + intros. rewrite <- H. eapply match_transform_program; eauto. Qed. Definition trans_stackframe (msf: Mach.stackframe) : stackframe := |