diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
| commit | 579ce1d6d18371b753fff2dac7305e13b85b8cab (patch) | |
| tree | 68879b84ccfabf0424178c4ad046ebd97461d8c2 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 3be0a8daa9ed0e787d1e4b26092aea4a496b88fd (diff) | |
| download | compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.tar.gz compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.zip | |
generalize bblock_equiv into bblock_simu
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f470ef8a..5d4fc881 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -741,7 +741,7 @@ Proof. eapply transf_function_no_overflow; eauto. erewrite transf_exec_bblock in H2; eauto. - inv BBEQ. rewrite H3 in H2. + unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence. exists (State rs' m'). split; try (constructor; auto). eapply transf_step_simu; eauto. |