# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1499881786 14400
# Node ID 16d701d4bd8222bb6303799c12ae17cd71ae7155
# Parent  a43fd2ba7ad3682789e915ec931ffab2e0ce1d11
And working with 8.6 again

diff -r a43fd2ba7ad3 -r 16d701d4bd82 src/GeneralRec.v
--- 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.
diff -r a43fd2ba7ad3 -r 16d701d4bd82 src/Intro.v
--- a/src/Intro.v	Wed Jul 12 13:33:23 2017 -0400
+++ b/src/Intro.v	Wed Jul 12 13:49:46 2017 -0400
@@ -186,7 +186,7 @@
 (** ** Installation and Emacs Set-Up *)
 
 (**
-At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.4pl5 and 8.5beta2.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
+At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.4pl6, 8.5pl3, and 8.6.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
 
 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.