changeset 563:af97676583f3 tip

Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -0500
parents 36b1f893c1e0
children
files .hgignore _CoqProject src/GeneralRec.v src/Intro.v src/MoreDep.v src/StackMachine.v src/Subset.v src/Universes.v
diffstat 8 files changed, 13 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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
--- /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
--- 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 *)
--- 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.
 
--- 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 *)
--- 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.
 
 (** <<
--- 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 *)
--- 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