From e8c1980257308dc8e5786c8d70b669c8d24b213f Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 18 Nov 2017 11:45:26 -0500
Subject: [PATCH] Working with Coq 8.5pl2 again

---
 CompilerCorrectness.v          | 4 +++-
 CompilerCorrectness_template.v | 4 +++-
 DependentInductiveTypes.v      | 2 +-
 SubsetTypes.v                  | 9 ++++++++-
 frap_book.tex                  | 2 +-
 5 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v
index 5732357..d0b3b45 100644
--- a/CompilerCorrectness.v
+++ b/CompilerCorrectness.v
@@ -350,7 +350,9 @@ Proof.
   invert 1; invert 1; simplify.
   eapply plug_deterministic in H0; eauto.
   invert H0.
-  eapply deterministic0 in H1; eauto.
+  match goal with
+  | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto
+  end.
   propositional; subst; auto.
   invert H0.
   auto.
diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v
index 2a97c20..577f958 100644
--- a/CompilerCorrectness_template.v
+++ b/CompilerCorrectness_template.v
@@ -280,7 +280,9 @@ Proof.
   invert 1; invert 1; simplify.
   eapply plug_deterministic in H0; eauto.
   invert H0.
-  eapply deterministic0 in H1; eauto.
+  match goal with
+  | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto
+  end.
   propositional; subst; auto.
   invert H0.
   auto.
diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v
index f006580..526d2c2 100644
--- a/DependentInductiveTypes.v
+++ b/DependentInductiveTypes.v
@@ -1159,7 +1159,7 @@ Section split.
   Defined.
 End split.
 
-Arguments split [P1 P2].
+Implicit Arguments split [P1 P2].
 
 (* And now, a few more boring lemmas.  Rejoin at "BOREDOM VANQUISHED", if you
  * like. *)
diff --git a/SubsetTypes.v b/SubsetTypes.v
index 7c3fe32..02838d0 100644
--- a/SubsetTypes.v
+++ b/SubsetTypes.v
@@ -613,7 +613,14 @@ Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~
         [||TBool||]
     end); simplify; propositional; subst; eauto;
     match goal with
-    | [ H : hasType _ _ |- _ ] => invert2 H
+    | [ H : hasType ?x _ |- _ ] =>
+      match goal with
+      | [ y : _ |- _ ] =>
+        match y with
+        | x => fail 2
+        end
+      | _ => invert2 H
+      end
     end; eauto.
 Defined.
 
diff --git a/frap_book.tex b/frap_book.tex
index c765b42..f7e767e 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4811,7 +4811,7 @@ The project home page is:
 \begin{center}
   \url{https://coq.inria.fr/}
 \end{center}
-The code associated with this book is designed to work with Coq versions 8.4 and higher.
+The code associated with this book is designed to work with Coq versions 8.5 and higher.
 The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
 We assume that readers have installed Coq by one of those means or another.
 It will also be almost essential to use some graphical interface for Coq editing.