# HG changeset patch # User Adam Chlipala # Date 1503159280 14400 # Node ID 93471096cdd453727bfb60d90dab9933b843f2a2 # Parent cb81f74d8c92d084cda60cb11f4a1c1980cddac3# Parent c8d01fb69970e1c142565c97a9e3f96227b96c76 Merge diff -r cb81f74d8c92 -r 93471096cdd4 latex/cpdt.tex --- a/latex/cpdt.tex Sat Aug 19 12:14:26 2017 -0400 +++ b/latex/cpdt.tex Sat Aug 19 12:14:40 2017 -0400 @@ -27,7 +27,7 @@ \mbox{}\vfill \begin{center} -Copyright Adam Chlipala 2008-2013, 2015. +Copyright Adam Chlipala 2008-2013, 2015, 2017. This work is licensed under a diff -r cb81f74d8c92 -r 93471096cdd4 src/GeneralRec.v --- a/src/GeneralRec.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/GeneralRec.v Sat Aug 19 12:14:40 2017 -0400 @@ -822,10 +822,7 @@ 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. + try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *) crush. inversion H; clear H; crush. eauto. @@ -839,10 +836,7 @@ 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. + try subst A. (* Same as above *) crush. inversion H0; clear H0; crush. eauto. diff -r cb81f74d8c92 -r 93471096cdd4 src/Intro.v --- a/src/Intro.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Intro.v Sat Aug 19 12:14:40 2017 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2013, 2015, Adam Chlipala +(* Copyright (c) 2008-2013, 2015, 2017, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -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.4pl5 and 8.5beta2. 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.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. %\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 cb81f74d8c92 -r 93471096cdd4 src/Match.v --- a/src/Match.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Match.v Sat Aug 19 12:14:40 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{%##map##%}%. *) 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) diff -r cb81f74d8c92 -r 93471096cdd4 src/Reflection.v --- a/src/Reflection.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Reflection.v Sat Aug 19 12:14:40 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 diff -r cb81f74d8c92 -r 93471096cdd4 src/Universes.v --- a/src/Universes.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Universes.v Sat Aug 19 12:14:40 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 diff -r cb81f74d8c92 -r 93471096cdd4 staging/updates.rss --- a/staging/updates.rss Sat Aug 19 12:14:26 2017 -0400 +++ b/staging/updates.rss Sat Aug 19 12:14:40 2017 -0400 @@ -12,6 +12,14 @@ http://blogs.law.harvard.edu/tech/rss + Book source updated for Coq 8.6 + Wed, 12 Jul 2017 14:56:07 EDT + http://adam.chlipala.net/cpdt/ + adamc@csail.mit.edu + The online versions of the book have been updated with code that builds with Coq 8.6, the latest version, as well as old versions 8.4 and 8.5. + + + Book source updated for Coq 8.5 Wed, 5 Aug 2015 18:08:34 EDT http://adam.chlipala.net/cpdt/