diff options
Diffstat (limited to 'mppa_k1c/lib/Machblockgenproof.v')
-rw-r--r-- | mppa_k1c/lib/Machblockgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v index 77db094d..02d154c7 100644 --- a/mppa_k1c/lib/Machblockgenproof.v +++ b/mppa_k1c/lib/Machblockgenproof.v @@ -719,17 +719,17 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2:{ destruct i; simpl in * |- *; try congruence. } + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ). exists nil; simpl; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. - 10: {exists (add_to_new_bblock (MB_basic bi)::nil). exists b. + Focus 10. exists (add_to_new_bblock (MB_basic bi)::nil). exists b. cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. eapply End_basic. inversion H; try(simpl; congruence). - simpl in H5; congruence. } + simpl in H5; congruence. all: try(exists nil; simpl; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). - (*i=cfi*) destruct i; try(simpl in Heqti; congruence). |