# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1499880803 14400
# Node ID a43fd2ba7ad3682789e915ec931ffab2e0ce1d11
# Parent  2c8c693ddaba698f71b86d5e2b58e365c3b809ea
Working again with Coq 8.4

diff -r 2c8c693ddaba -r a43fd2ba7ad3 src/GeneralRec.v
--- a/src/GeneralRec.v	Wed Jul 12 13:08:24 2017 -0400
+++ b/src/GeneralRec.v	Wed Jul 12 13:33:23 2017 -0400
@@ -822,6 +822,7 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
+  subst B.
   crush.
   inversion H; clear H; crush.
   eauto.
@@ -835,6 +836,7 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
+  subst A.
   crush.
   inversion H0; clear H0; crush.
   eauto.