diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-13 17:43:27 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-13 17:43:27 +0200 |
| commit | a1b4ed93ca2b7a244fb5d6d54c0bd0737f618837 (patch) | |
| tree | 6fe88e7f1885010babdc5eb0ee3275b9033c837b | |
| parent | c4496c4c63a01b2a7c1b89cca128ce0b55b50c29 (diff) | |
| download | compcert-kvx-a1b4ed93ca2b7a244fb5d6d54c0bd0737f618837.tar.gz compcert-kvx-a1b4ed93ca2b7a244fb5d6d54c0bd0737f618837.zip | |
Compatibility fix for Coq 8.7.1
| -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 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). |