Mercurial > cpdt > repo
diff src/GeneralRec.v @ 549:16d701d4bd82
And working with 8.6 again
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 12 Jul 2017 13:49:46 -0400 |
parents | a43fd2ba7ad3 |
children | af97676583f3 |
line wrap: on
line diff
--- a/src/GeneralRec.v Wed Jul 12 13:33:23 2017 -0400 +++ b/src/GeneralRec.v Wed Jul 12 13:49:46 2017 -0400 @@ -822,7 +822,7 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - subst B. + 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. @@ -836,7 +836,7 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - subst A. + try subst A. (* Same as above *) crush. inversion H0; clear H0; crush. eauto.