# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1515344011 18000
# Node ID af97676583f37e3f6814839a98051beff89054f9
# Parent  36b1f893c1e0e6b68c460bc7dd03cf40026b3d53
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6

diff -r 36b1f893c1e0 -r af97676583f3 .hgignore
--- a/.hgignore	Mon Dec 18 17:05:53 2017 -0500
+++ b/.hgignore	Sun Jan 07 11:53:31 2018 -0500
@@ -5,6 +5,7 @@
 *.depend
 *.vo
 Makefile.coq
+Makefile.coq.conf
 .coq_globals
 
 */coqdoc.sty
diff -r 36b1f893c1e0 -r af97676583f3 _CoqProject
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/_CoqProject	Sun Jan 07 11:53:31 2018 -0500
@@ -0,0 +1,1 @@
+-R src Cpdt
diff -r 36b1f893c1e0 -r af97676583f3 src/GeneralRec.v
--- a/src/GeneralRec.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/GeneralRec.v	Sun Jan 07 11:53:31 2018 -0500
@@ -12,6 +12,8 @@
 
 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
 
+Require Extraction.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 (* end hide *)
diff -r 36b1f893c1e0 -r af97676583f3 src/Intro.v
--- a/src/Intro.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/Intro.v	Sun Jan 07 11:53:31 2018 -0500
@@ -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.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.
+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.6.1 and 8.7.1.  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.
 
diff -r 36b1f893c1e0 -r af97676583f3 src/MoreDep.v
--- a/src/MoreDep.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/MoreDep.v	Sun Jan 07 11:53:31 2018 -0500
@@ -12,6 +12,8 @@
 
 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
 
+Require Extraction.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 (* end hide *)
diff -r 36b1f893c1e0 -r af97676583f3 src/StackMachine.v
--- a/src/StackMachine.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/StackMachine.v	Sun Jan 07 11:53:31 2018 -0500
@@ -850,6 +850,7 @@
 
 (** It is probably worth emphasizing that we are doing more than building mathematical models.  Our compilers are functional programs that can be executed efficiently.  One strategy for doing so is based on%\index{program extraction}% _program extraction_, which generates OCaml code from Coq developments.  For instance, we run a command to output the OCaml version of [tcompile]:%\index{Vernacular commands!Extraction}% *)
 
+Require Extraction.
 Extraction tcompile.
 
 (** <<
diff -r 36b1f893c1e0 -r af97676583f3 src/Subset.v
--- a/src/Subset.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/Subset.v	Sun Jan 07 11:53:31 2018 -0500
@@ -12,6 +12,8 @@
 
 Require Import Cpdt.CpdtTactics.
 
+Require Extraction.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 (* end hide *)
diff -r 36b1f893c1e0 -r af97676583f3 src/Universes.v
--- a/src/Universes.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/Universes.v	Sun Jan 07 11:53:31 2018 -0500
@@ -12,6 +12,8 @@
 
 Require Import DepList Cpdt.CpdtTactics.
 
+Require Extraction.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 (* end hide *)
@@ -1070,7 +1072,7 @@
 
   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. *)
+                     * 8.4 and 8.5. *)
 (** %\vspace{-.15in}%[[
   H : proof p
   H1 : And p q = And p0 q0