--- a/src/GeneralRec.v	Thu May 12 18:09:36 2016 -0500
+++ b/src/GeneralRec.v	Wed Jul 12 13:08:24 2017 -0400
@@ -822,10 +822,6 @@
   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.
   crush.
   inversion H; clear H; crush.
   eauto.
@@ -839,10 +835,6 @@
   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.
   crush.
   inversion H0; clear H0; crush.
   eauto.

--- a/src/Match.v	Thu May 12 18:09:36 2016 -0500
+++ b/src/Match.v	Wed Jul 12 13:08:24 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	Thu May 12 18:09:36 2016 -0500
+++ b/src/Reflection.v	Wed Jul 12 13:08:24 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	Thu May 12 18:09:36 2016 -0500
+++ b/src/Universes.v	Wed Jul 12 13:08:24 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