Mercurial > cpdt > repo
diff src/GeneralRec.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 16d701d4bd82 |
children | af97676583f3 |
line wrap: on
line diff
--- a/src/GeneralRec.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/GeneralRec.v Sat Aug 19 12:14:40 2017 -0400 @@ -822,10 +822,7 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - move H3 after A. - generalize dependent B0. - do 2 intro. - subst. + try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *) crush. inversion H; clear H; crush. eauto. @@ -839,10 +836,7 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - move H3 after B. - generalize dependent B0. - do 2 intro. - subst. + try subst A. (* Same as above *) crush. inversion H0; clear H0; crush. eauto.