From a1b4ed93ca2b7a244fb5d6d54c0bd0737f618837 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 13 Sep 2019 17:43:27 +0200 Subject: Compatibility fix for Coq 8.7.1 --- mppa_k1c/lib/Machblockgenproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v index 9186e54a..ab7fff74 100644 --- a/mppa_k1c/lib/Machblockgenproof.v +++ b/mppa_k1c/lib/Machblockgenproof.v @@ -715,17 +715,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). -- cgit