--- a/latex/cpdt.tex	Sat Aug 19 12:14:26 2017 -0400
+++ b/latex/cpdt.tex	Sat Aug 19 12:14:40 2017 -0400
@@ -27,7 +27,7 @@
 \mbox{}\vfill
 \begin{center}
 
-Copyright Adam Chlipala 2008-2013, 2015.
+Copyright Adam Chlipala 2008-2013, 2015, 2017.
 
 
 This work is licensed under a

--- 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.

--- a/src/Intro.v	Sat Aug 19 12:14:26 2017 -0400
+++ b/src/Intro.v	Sat Aug 19 12:14:40 2017 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2013, 2015, Adam Chlipala
+(* Copyright (c) 2008-2013, 2015, 2017, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -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.
 

--- a/src/Match.v	Sat Aug 19 12:14:26 2017 -0400
+++ b/src/Match.v	Sat Aug 19 12:14:40 2017 -0400
@@ -444,7 +444,7 @@
 Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking %\coqdocvar{%#<tt>#map#</tt>#%}%. *)
 
 Goal False.
-  let ls := map (nat * nat)%type ltac:(fun x => constr:(x, x)) (1 :: 2 :: 3 :: nil) in
+  let ls := map (nat * nat)%type ltac:(fun x => constr:((x, x))) (1 :: 2 :: 3 :: nil) in
     pose ls.
   (** [[
   l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)

--- a/src/Reflection.v	Sat Aug 19 12:14:26 2017 -0400
+++ b/src/Reflection.v	Sat Aug 19 12:14:40 2017 -0400
@@ -673,7 +673,7 @@
   let b := inList x xs in
     match b with
       | true => xs
-      | false => constr:(x, xs)
+      | false => constr:((x, xs))
     end.
 
 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *)
@@ -718,8 +718,8 @@
 
 Ltac reifyTerm xs e :=
   match e with
-    | True => constr:Truth'
-    | False => constr:Falsehood'
+    | True => Truth'
+    | False => Falsehood'
     | ?e1 /\ ?e2 =>
       let p1 := reifyTerm xs e1 in
       let p2 := reifyTerm xs e2 in

--- a/src/Universes.v	Sat Aug 19 12:14:26 2017 -0400
+++ b/src/Universes.v	Sat Aug 19 12:14:40 2017 -0400
@@ -1068,7 +1068,9 @@
 
   The first goal looks reasonable.  Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
 
-  discriminate.
+  try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically!
+                     * This line left here to keep everything working in
+                     * 8.4, 8.5, and 8.6. *)
 (** %\vspace{-.15in}%[[
   H : proof p
   H1 : And p q = And p0 q0

--- a/staging/updates.rss	Sat Aug 19 12:14:26 2017 -0400
+++ b/staging/updates.rss	Sat Aug 19 12:14:40 2017 -0400
@@ -12,6 +12,14 @@
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
 <item>
+        <title>Book source updated for Coq 8.6</title>
+        <pubDate>Wed, 12 Jul 2017 14:56:07 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>The online versions of the book have been updated with code that builds with Coq 8.6, the latest version, as well as old versions 8.4 and 8.5.</description>
+</item>
+
+<item>
         <title>Book source updated for Coq 8.5</title>
         <pubDate>Wed, 5 Aug 2015 18:08:34 EDT</pubDate>
         <link>http://adam.chlipala.net/cpdt/</link>