Mercurial > cpdt > repo
changeset 563:af97676583f3
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 | 5504235ea06d |
| 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