Get it to build with Coq 8.4

src/GeneralRec.v

-(* Copyright (c) 2006, 2011, Adam Chlipala
+(* Copyright (c) 2006, 2011-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -346,6 +346,11 @@ Hint Resolve ex_irrelevant.
 
 Require Import Max.
 
+Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
+  induction n; destruct m; simpl; intuition;
+    specialize (IHn m); intuition.
+Qed.
+
 Ltac max := intros n m; generalize (max_spec_le n m); crush.
 
 Lemma max_1 : forall n m, max n m >= n.

src/Intro.v

@@ -183,7 +183,7 @@ Some readers have asked about the pragmatics of using this tactic library in the
 (** ** 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 version 8.3pl2, though parts may work with other 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.3pl2 and 8.4 beta, though parts may work with other versions.
 
 %\index{Proof General|(}%To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
 

src/MoreDep.v

@@ -558,13 +558,13 @@ Notation "{< x >}" := (existT _ _ x).
 Definition balance1 n (a : rtree n) (data : nat) c2 :=
   match a in rtree n return rbtree c2 n
     -> { c : color & rbtree c (S n) } with
-    | RedNode' _ _ _ t1 y t2 =>
-      match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+    | RedNode' _ c0 _ t1 y t2 =>
+      match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
         -> { c : color & rbtree c (S n) } with
         | RedNode _ a x b => fun c d =>
           {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
         | t1' => fun t2 =>
-          match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+          match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
             -> { c : color & rbtree c (S n) } with
             | RedNode _ b x c => fun a d =>
               {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
@@ -581,13 +581,13 @@ Definition balance1 n (a : rtree n) (data : nat) c2 :=
 
 Definition balance2 n (a : rtree n) (data : nat) c2 :=
   match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
-    | RedNode' _ _ _ t1 z t2 =>
-      match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+    | RedNode' _ c0 _ t1 z t2 =>
+      match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
         -> { c : color & rbtree c (S n) } with
         | RedNode _ b y c => fun d a =>
           {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
         | t1' => fun t2 =>
-          match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+          match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
             -> { c : color & rbtree c (S n) } with
             | RedNode _ c z' d => fun b a =>
               {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
@@ -1132,7 +1132,11 @@ Section dec_star.
       + {forall l', S l' <= l
         -> ~ P (substring n (S l') s)
         \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
-      match l with
+      match l return {exists l', S l' <= l
+        /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+      + {forall l', S l' <= l
+        -> ~ P (substring n (S l') s)
+        \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} with
         | O => _
         | S l' =>
           (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
@@ -1186,13 +1190,10 @@ Section dec_star.
     end.
   Defined.
 
-  (** Finally, we have [dec_star].  It has a straightforward implementation.  We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star].  The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
+  (** Finally, we have [dec_star], defined by straightforward reduction from [dec_star']. *)
 
   Definition dec_star : {star P s} + {~ star P s}.
-    refine (match s return _ with
-              | "" => Reduce (dec_star' (n := length s) 0 _)
-              | _ => Reduce (dec_star' (n := length s) 0 _)
-            end); crush.
+    refine (Reduce (dec_star' (n := length s) 0 _)); crush.
   Defined.
 End dec_star.
 
@@ -1226,22 +1227,22 @@ Defined.
 
 (* begin hide *)
 Example hi := Concat (Char "h"%char) (Char "i"%char).
-Eval simpl in matches hi "hi".
-Eval simpl in matches hi "bye".
+Eval hnf in matches hi "hi".
+Eval hnf in matches hi "bye".
 
 Example a_b := Or (Char "a"%char) (Char "b"%char).
-Eval simpl in matches a_b "".
-Eval simpl in matches a_b "a".
-Eval simpl in matches a_b "aa".
-Eval simpl in matches a_b "b".
+Eval hnf in matches a_b "".
+Eval hnf in matches a_b "a".
+Eval hnf in matches a_b "aa".
+Eval hnf in matches a_b "b".
 (* end hide *)
 
-(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer. *)
+(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer.  We use evaluation strategy %\index{tactics!hnf}%[hnf] to reduce each term to %\index{head-normal form}\emph{%#<i>#head-normal form#</i>#%}%, where the datatype constructor used to build its value is known. *)
 
 Example a_star := Star (Char "a"%char).
-Eval simpl in matches a_star "".
-Eval simpl in matches a_star "a".
-Eval simpl in matches a_star "b".
-Eval simpl in matches a_star "aa".
+Eval hnf in matches a_star "".
+Eval hnf in matches a_star "a".
+Eval hnf in matches a_star "b".
+Eval hnf in matches a_star "aa".
 
 (** Evaluation inside Coq does not scale very well, so it is easy to build other tests that run for hours or more.  Such cases are better suited to execution with the extracted OCaml code. *)

src/Subset.v

-(* Copyright (c) 2008-2011, Adam Chlipala
+(* Copyright (c) 2008-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -566,7 +566,7 @@ Notation "[| x |]" := (Found _ x _).
 
 Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
   refine (fun n =>
-    match n with
+    match n return {{m | n = S m}} with
       | O => ??
       | S n' => [|n'|]
     end); trivial.
@@ -725,7 +725,7 @@ Definition typeCheck : forall e : exp, {{t | hasType e t}}.
   Hint Constructors hasType.
 
   refine (fix F (e : exp) : {{t | hasType e t}} :=
-    match e with
+    match e return {{t | hasType e t}} with
       | Nat _ => [|TNat|]
       | Plus e1 e2 =>
         t1 <- F e1;
@@ -872,7 +872,7 @@ Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~
   (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *)
 
   refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=
-    match e with
+    match e return {t : type | hasType e t} + {forall t, ~ hasType e t} with
       | Nat _ => [||TNat||]
       | Plus e1 e2 =>
         t1 <-- F e1;

staging/index.html

@@ -39,11 +39,11 @@
 <div class="project">
 <h2>Status</h2>
 
-<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, and then again on January 14, 2011 to support Coq 8.3.  On August 25, 2011, I've started passes through all chapters, with an eye toward getting ready both for <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">my fall class</a> and publication by MIT Press.  I'm adding bibliographic references, index entries, and additional exercises, along with the usual tweaks and improvements.</p>
+<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, then again on January 14, 2011 to support Coq 8.3, and then again on March 29, 2012 to support Coq 8.4 beta.  On August 25, 2011, I started passes through all chapters, with an eye toward getting ready both for <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">my fall class</a> and publication by MIT Press.  I'm adding bibliographic references and index entries, along with the usual tweaks and improvements.</p>
 
 <p>The current version is effectively a beta release.  It is intended to be consistent, self-contained, and useful, both for individual study and for introductory theorem-proving classes aimed at students with ML or Haskell experience and with basic familiarity with programming language theory.</p>
 
-<p>The main omissions have to do with some supporting resources that I didn't get around to implementing when I used this book for a course.  Some suggested exercises are present, but only at points where I was looking to assign an exercise in the course.  Some chapters are lacking the annotations used to build reduced versions of their source code, where some definitions and proofs have been elided; the course instructor can step through such a file, guiding class participants in filling in the omitted code.</p>
+<p>The main omissions have to do with some supporting resources that I didn't get around to implementing when I used this book for a course.  Some suggested exercises are present (now only in a supplementary file), but only at points where I was looking to assign an exercise in the course.  Some chapters are lacking the annotations used to build reduced versions of their source code, where some definitions and proofs have been elided; the course instructor can step through such a file, guiding class participants in filling in the omitted code.</p>
 
 <p>Previous versions included a final Part on programming language semantics in particular.  I have decided to separate that part out.  I plan to put it up as a supplementary resource eventually; for now it is simply removed.  (It remains present in the <a href="repo">Mercurial</a> history.)</p>
 </div>

staging/updates.rss

@@ -11,6 +11,13 @@
 <webMaster>adam@chlipala.net</webMaster>
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
+<item>
+        <title>Update to work with Coq 8.4 beta (and keep working with 8.3pl2)</title>
+        <pubDate>Thu, 29 Mar 2012 18:10:00 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+</item>
+
 <item>
         <title>Two new tricks useful in proof by reflection</title>
         <pubDate>Thu, 29 Mar 2012 17:12:01 EDT</pubDate>