--- a/src/MoreDep.v	Wed Nov 28 19:33:21 2012 -0500
+++ b/src/MoreDep.v	Fri Nov 30 11:57:55 2012 -0500
@@ -106,7 +106,7 @@
 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
 >>
 
-Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a <<Match>> exception to be thrown.  In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors.  It is educational to discover such an encoding for ourselves.  We might try using an [in] clause somehow.
+Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a <<Match>> exception to be thrown.  In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors; the error message above was generated by an older Coq version.  It is educational to discover for ourselves the encoding that the most recent Coq versions use.  We might try using an [in] clause somehow.
 
 [[
   Definition hd n (ls : ilist (S n)) : A :=
@@ -158,15 +158,15 @@
 
 We come now to the one rule of dependent pattern matching in Coq.  A general dependent pattern match assumes this form (with unnecessary parentheses included to make the syntax easier to parse):
 [[
-  match E in (T x1 ... xn) as y return U with
+  match E as y in (T x1 ... xn) return U with
     | C z1 ... zm => B
     | ...
   end
 ]]
 
-The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments.  An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E].  An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E].
+The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments.  An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E].  An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E].
 
-We bind these new variables [xi] and [y] so that they may be referred to in [U], a type given in the %\index{return clause}%[return] clause.  The overall type of the [match] will be [U], with [E] substituted for [y], and with each [xi] substituted by the actual argument appearing in that position within [E]'s type.
+We bind these new variables [y] and [xi] so that they may be referred to in [U], a type given in the %\index{return clause}%[return] clause.  The overall type of the [match] will be [U], with [E] substituted for [y], and with each [xi] substituted by the actual argument appearing in that position within [E]'s type.
 
 In general, each case of a [match] may have a pattern built up in several layers from the constructors of various inductive type families.  To keep this exposition simple, we will focus on patterns that are just single applications of inductive type constructors to lists of variables.  Coq actually compiles the more general kind of pattern matching into this more restricted kind automatically, so understanding the typing of [match] requires understanding the typing of [match]es lowered to match one constructor at a time.
 
@@ -378,13 +378,13 @@
 
     Coq gives us another cryptic error message.  Like so many others, this one basically means that Coq is not able to build some proof about dependent types.  It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code.  We will encounter many examples of case-specific tricks for recovering from errors like this one.
 
-    For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book's [CpdtTactics] module.  General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed.  The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq.  In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box.  (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
+    For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book's [CpdtTactics] module.  General elimination/inversion of dependently typed hypotheses is undecidable, as witnessed by a simple reduction to the known-undecidable problem of higher-order unification, which has come up a few times already.  The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq.  In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dependent destruction]'s implementation, but for now, we treat it as a useful black box.  (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
   
   dep_destruct (cfold e1).
 
   (** This successfully breaks the subgoal into 5 new subgoals, one for each constructor of [exp] that could produce an [exp Nat].  Note that [dep_destruct] is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like [hd] and [pairOut].
 
-     This is the only new trick we need to learn to complete the proof.  We can back up and give a short, automated proof. *)
+     This is the only new trick we need to learn to complete the proof.  We can back up and give a short, automated proof (which again is safe to skip and uses Ltac features not introduced yet). *)
 
   Restart.
 
@@ -786,7 +786,7 @@
     -> star (s1 ++ s2).
 End star.
 
-(** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings.  Here is a reasonable-looking definition that is restricted to constant characters and concatenation.  We use the constructor [String], which is the analogue of list cons for the type [string], where [""] is like list nil.
+(** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings, such that the index of a [regexp] tells us which language (string predicate) it recognizes.  Here is a reasonable-looking definition that is restricted to constant characters and concatenation.  We use the constructor [String], which is the analogue of list cons for the type [string], where [""] is like list nil.
 [[
 Inductive regexp : (string -> Prop) -> Set :=
 | Char : forall ch : ascii,
@@ -1115,23 +1115,19 @@
         -> ~ P (substring n (S l') s)
         \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
       refine (fix F (l : nat) : {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)} :=
-      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') _)
-          || F l'
-      end); clear F; crush; eauto 7;
-      match goal with
-        | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
-      end.
+          /\ 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)} :=
+        match l with
+          | O => _
+          | S l' =>
+            (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
+            || F l'
+        end); clear F; crush; eauto 7;
+        match goal with
+          | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
+        end.
     Defined.
   End dec_star''.