diff options
Diffstat (limited to 'kvx/lib/Machblockgen.v')
| -rw-r--r-- | kvx/lib/Machblockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v index 3d5d7b2c..5a2f2a61 100644 --- a/kvx/lib/Machblockgen.v +++ b/kvx/lib/Machblockgen.v @@ -155,11 +155,11 @@ Proof. + intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence. + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. * eapply Tr_add_basic; eauto. - * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. + * replace (add_basic bi empty_bblock) with (add_to_new_bblock (MB_basic bi)); auto. rewrite Heqti; eapply Tr_end_block; eauto. rewrite <- Heqti. eapply End_basic. congruence. + intros. - cutrewrite (cfi_bblock cfi = add_to_new_bblock (MB_cfi cfi)); auto. + replace (cfi_bblock cfi) with (add_to_new_bblock (MB_cfi cfi)); auto. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <- Heqti. eapply End_cfi. congruence. Qed. |