--- a/src/DataStruct.v	Wed Nov 28 19:33:21 2012 -0500
+++ b/src/DataStruct.v	Fri Nov 30 11:57:55 2012 -0500
@@ -41,7 +41,7 @@
   | First : forall n, fin (S n)
   | Next : forall n, fin n -> fin (S n).
 
-  (** An instance of [fin] is essentially a more richly typed copy of the natural numbers.  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
+  (** An instance of [fin] is essentially a more richly typed copy of a prefix of the natural numbers.  The type [fin n] is isomorphic to [{m : nat | m < n}].  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
 
      Now it is easy to pick a [Prop]-free type for a selection function.  As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
      [[
@@ -55,7 +55,7 @@
         end
     end.
     ]]
-    %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
+    %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return], with the [return] clause chosen carefully so that it returns the proper type [A] in case the [fin] index is [O], which we know is true here; and so that it returns an easy-to-inhabit type [unit] in the remaining, impossible cases, which nonetheless appear explicitly in the body of the [match].
     [[
   Fixpoint get n (ls : ilist n) : fin n -> A :=
     match ls with
@@ -200,7 +200,7 @@
   | HNil : hlist nil
   | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
 
-  (** We can implement a variant of the last section's [get] function for [hlist]s.  To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *)
+  (** We can implement a variant of the last section's [get] function for [hlist]s.  To get the dependent typing to work out, we will need to index our element selectors (in type family [member]) by the types of data that they point to.%\index{Gallina terms!member}% *)
 
 (* end thide *)
   (* EX: Define an analogue to [get] for [hlist]s. *)
@@ -248,7 +248,7 @@
 Implicit Arguments HNext [A elm x ls].
 (* end thide *)
 
-(** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
+(** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
 
 Definition someTypes : list Set := nat :: bool :: nil.
 
@@ -370,7 +370,7 @@
 
 (** * Recursive Type Definitions *)
 
-(** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above.  Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions. *)
+(** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above.  Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions.  Here we will preface type names with the letter [f] to indicate that they are based on explicit recursive _function_ definitions. *)
 
 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
 

--- a/src/Equality.v	Wed Nov 28 19:33:21 2012 -0500
+++ b/src/Equality.v	Fri Nov 30 11:57:55 2012 -0500
@@ -180,7 +180,7 @@
 
 (** * Heterogeneous Lists Revisited *)
 
-(** One of our example dependent data structures from the last chapter was the heterogeneous list and its associated "cursor" type.  The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
+(** One of our example dependent data structures from the last chapter (code repeated below) was the heterogeneous list and its associated "cursor" type.  The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
 
 Section fhlist.
   Variable A : Type.
@@ -420,7 +420,7 @@
      : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
      ]]
 
-     The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
+     The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  (Its name uses the acronym "UIP" for "unicity of identity proofs.")  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
 
 (* begin hide *)
   Import Eq_rect_eq.
@@ -459,16 +459,15 @@
   (* end thide *)
   (* end hide *)
 
-  Print Streicher_K.
+  Check Streicher_K.
 (* end thide *)
 (** %\vspace{-.15in}% [[
-Streicher_K = 
-fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
+Streicher_K
      : forall (U : Type) (x : U) (P : x = x -> Prop),
-       P (eq_refl x) -> forall p : x = x, P p
+       P eq_refl -> forall p : x = x, P p
   ]]
 
-  This is the unfortunately named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
+  This is the opaquely named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
 
 End fhlist_map.
 
@@ -691,7 +690,7 @@
     JMeq_refl : JMeq x x
     ]]
 
-The identifier [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics.  The definition [JMeq] starts out looking a lot like the definition of [eq].  The crucial difference is that we may use [JMeq] _on arguments of different types_.  For instance, a lemma that we failed to establish before is trivial with [JMeq].  It makes for prettier theorem statements to define some syntactic shorthand first. *)
+The identifier [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as an inside joke about British politics.  The definition [JMeq] starts out looking a lot like the definition of [eq].  The crucial difference is that we may use [JMeq] _on arguments of different types_.  For instance, a lemma that we failed to establish before is trivial with [JMeq].  It makes for prettier theorem statements to define some syntactic shorthand first. *)
 
 Infix "==" := JMeq (at level 70, no associativity).
 
@@ -722,7 +721,7 @@
      : forall (A : Type) (x y : A), x == y -> x = y
     ]]
 
-    It may be surprising that we cannot prove that heterogeneous equality implies normal equality.  The difficulties are the same kind we have seen so far, based on limitations of [match] annotations.
+    It may be surprising that we cannot prove that heterogeneous equality implies normal equality.  The difficulties are the same kind we have seen so far, based on limitations of [match] annotations.  The [JMeq_eq] axiom has been proved on paper to be consistent, but asserting it may still be considered to complicate the logic we work in, so there is some motivation for avoiding it.
 
    We can redo our [fhapp] associativity proof based around [JMeq]. *)
 
@@ -862,7 +861,7 @@
   -> S n == S m.
   intros n m H.
 
-  (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. *)
+  (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract.  (In general, [pattern] abstracts over a term by introducing a new anonymous function taking that term as argument.) *)
 
   pattern n.
   (** %\vspace{-.15in}%[[

--- a/src/GeneralRec.v	Wed Nov 28 19:33:21 2012 -0500
+++ b/src/GeneralRec.v	Fri Nov 30 11:57:55 2012 -0500
@@ -56,14 +56,14 @@
       | h :: ls' => insert h (merge ls' ls2)
     end.
 
-  (** The last helper function for classic merge sort is the one that follows, to partition a list arbitrarily into two pieces of approximately equal length. *)
+  (** The last helper function for classic merge sort is the one that follows, to split a list arbitrarily into two pieces of approximately equal length. *)
 
-  Fixpoint partition (ls : list A) : list A * list A :=
+  Fixpoint split (ls : list A) : list A * list A :=
     match ls with
       | nil => (nil, nil)
       | h :: nil => (h :: nil, nil)
       | h1 :: h2 :: ls' =>
-	let (ls1, ls2) := partition ls' in
+	let (ls1, ls2) := split ls' in
 	  (h1 :: ls1, h2 :: ls2)
     end.
 
@@ -72,13 +72,13 @@
   Fixpoint mergeSort (ls : list A) : list A :=
     if leb (length ls) 1
       then ls
-      else let lss := partition ls in
+      else let lss := split ls in
 	merge (mergeSort (fst lss)) (mergeSort (snd lss)).
 ]]
 
 <<
 Recursive call to mergeSort has principal argument equal to
-"fst (partition ls)" instead of a subterm of "ls".
+"fst (split ls)" instead of a subterm of "ls".
 >>
 
 The definition is rejected for not following the simple primitive recursion criterion.  In particular, it is not apparent that recursive calls to [mergeSort] are syntactic subterms of the original argument [ls]; indeed, they are not, yet we know this is a well-founded recursive definition.
@@ -171,35 +171,35 @@
 
   (** Notice that we end these proofs with %\index{Vernacular commands!Defined}%[Defined], not [Qed].  Recall that [Defined] marks the theorems as %\emph{transparent}%, so that the details of their proofs may be used during program execution.  Why could such details possibly matter for computation?  It turns out that [Fix] satisfies the primitive recursion restriction by declaring itself as _recursive in the structure of [Acc] proofs_.  This is possible because [Acc] proofs follow a predictable inductive structure.  We must do work, as in the last theorem's proof, to establish that all elements of a type belong to [Acc], but the automatic unwinding of those proofs during recursion is straightforward.  If we ended the proof with [Qed], the proof details would be hidden from computation, in which case the unwinding process would get stuck.
 
-     To justify our two recursive [mergeSort] calls, we will also need to prove that [partition] respects the [lengthOrder] relation.  These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation.  We use the syntax [@foo] to reference identifier [foo] with its implicit argument behavior turned off. *)
+     To justify our two recursive [mergeSort] calls, we will also need to prove that [split] respects the [lengthOrder] relation.  These proofs, too, must be kept transparent, to avoid stuckness of [Fix] evaluation.  We use the syntax [@foo] to reference identifier [foo] with its implicit argument behavior turned off.  (The proof details below use Ltac features not introduced yet, and they are safe to skip for now.) *)
 
-  Lemma partition_wf : forall len ls, 2 <= length ls <= len
-    -> let (ls1, ls2) := partition ls in
+  Lemma split_wf : forall len ls, 2 <= length ls <= len
+    -> let (ls1, ls2) := split ls in
       lengthOrder ls1 ls /\ lengthOrder ls2 ls.
     unfold lengthOrder; induction len; crush; do 2 (destruct ls; crush);
       destruct (le_lt_dec 2 (length ls));
         repeat (match goal with
                   | [ _ : length ?E < 2 |- _ ] => destruct E
                   | [ _ : S (length ?E) < 2 |- _ ] => destruct E
-                  | [ IH : _ |- context[partition ?L] ] =>
-                    specialize (IH L); destruct (partition L); destruct IH
+                  | [ IH : _ |- context[split ?L] ] =>
+                    specialize (IH L); destruct (split L); destruct IH
                 end; crush).
   Defined.
 
-  Ltac partition := intros ls ?; intros; generalize (@partition_wf (length ls) ls);
-    destruct (partition ls); destruct 1; crush.
+  Ltac split_wf := intros ls ?; intros; generalize (@split_wf (length ls) ls);
+    destruct (split ls); destruct 1; crush.
 
-  Lemma partition_wf1 : forall ls, 2 <= length ls
-    -> lengthOrder (fst (partition ls)) ls.
-    partition.
+  Lemma split_wf1 : forall ls, 2 <= length ls
+    -> lengthOrder (fst (split ls)) ls.
+    split_wf.
   Defined.
 
-  Lemma partition_wf2 : forall ls, 2 <= length ls
-    -> lengthOrder (snd (partition ls)) ls.
-    partition.
+  Lemma split_wf2 : forall ls, 2 <= length ls
+    -> lengthOrder (snd (split ls)) ls.
+    split_wf.
   Defined.
 
-  Hint Resolve partition_wf1 partition_wf2.
+  Hint Resolve split_wf1 split_wf2.
 
   (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually.  We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type.  (Note that we would not be able to complete the definition without this change, since [refine] will generate subgoals for the [if] branches based only on the _type_ of the test expression, not its _value_.) *)
 
@@ -209,7 +209,7 @@
       (fun (ls : list A)
         (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) =>
         if le_lt_dec 2 (length ls)
-	  then let lss := partition ls in
+	  then let lss := split ls in
             merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
 	  else ls)); subst lss; eauto.
   Defined.
@@ -226,7 +226,7 @@
 (* begin thide *)
 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
   mergeSort le ls = if le_lt_dec 2 (length ls)
-    then let lss := partition ls in
+    then let lss := split ls in
       merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
     else ls.
   intros; apply (Fix_eq (@lengthOrder_wf A) (fun _ => list A)); intros.
@@ -261,7 +261,7 @@
 let rec mergeSort le x =
   match le_lt_dec (S (S O)) (length x) with
   | Left ->
-    let lss = partition x in
+    let lss = split x in
     merge le (mergeSort le (fst lss)) (mergeSort le (snd lss))
   | Right -> x
 >>
@@ -382,7 +382,7 @@
 (* end hide *)
 (** remove printing exists *)
 
-(** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop.  For any approximation level, it fails to terminate (returns [None]).  Note the use of [abstract] to create a new opaque lemma for the proof found by the [run] tactic.  In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
+(** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop.  For any approximation level, it fails to terminate (returns [None]).  Note the use of [abstract] to create a new opaque lemma for the proof found by the #<tt>#%\coqdocvar{%run%}%#</tt># tactic.  In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior.  It is generally preferable to make proofs opaque when possible, as this enforces a kind of modularity in the code to follow, preventing it from depending on any details of the proof. *)
 
 Section Bottom.
   Variable A : Type.
@@ -570,7 +570,7 @@
     (fun (mergeSort : list A -> computation (list A))
       (ls : list A) =>
       if le_lt_dec 2 (length ls)
-	then let lss := partition ls in
+	then let lss := split ls in
           ls1 <- mergeSort (fst lss);
           ls2 <- mergeSort (snd lss);
           Return (merge le ls1 ls2)
@@ -605,7 +605,7 @@
 
 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
 
-   There are other theorems that are important to prove about combinators like [Return], [Bind], and [Fix].  In general, for a computation [c], we sometimes have a hypothesis proving [run c v] for some [v], and we want to perform inversion to deduce what [v] must be.  Each combinator should ideally have a theorem of that kind, for [c] built directly from that combinator.  We have omitted such theorems here, but they are not hard to prove.  In general, the domain theory-inspired approach avoids the type-theoretic "gotchas" that tend to show up in approaches that try to mix normal Coq computation with explicit syntax types.  The next section of this chapter demonstrates two alternate approaches of that sort. *)
+   There are other theorems that are important to prove about combinators like [Return], [Bind], and [Fix].  In general, for a computation [c], we sometimes have a hypothesis proving [run c v] for some [v], and we want to perform inversion to deduce what [v] must be.  Each combinator should ideally have a theorem of that kind, for [c] built directly from that combinator.  We have omitted such theorems here, but they are not hard to prove.  In general, the domain theory-inspired approach avoids the type-theoretic "gotchas" that tend to show up in approaches that try to mix normal Coq computation with explicit syntax types.  The next section of this chapter demonstrates two alternate approaches of that sort.  In the final section of the chapter, we review the pros and cons of the different choices, coming to the conclusion that none of them is obviously better than any one of the others for all situations. *)
 
 
 (** * Co-Inductive Non-Termination Monads *)
@@ -861,7 +861,7 @@
 
 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
   if le_lt_dec 2 (length ls)
-    then let lss := partition ls in
+    then let lss := split ls in
       ls1 <- mergeSort'' le (fst lss);
       ls2 <- mergeSort'' le (snd lss);
       Ret (merge le ls1 ls2)
@@ -912,7 +912,7 @@
 
    Another useful property is that a function and its termination argument may be developed separately.  We may even want to define functions that fail to terminate on some or all inputs.  The well-founded recursion technique does not have this property, but the other three do.
 
-   One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators.  This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader.
+   One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators.  This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader.  (For this and other details of notations, see Chapter 12 of the Coq 8.4 manual.)
 
    The first two techniques impose proof obligations that are more basic than termination arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity.  A function may not be defined, and thus may not be computed with, until these obligations are proved.  The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations.
 

--- a/src/Generic.v	Wed Nov 28 19:33:21 2012 -0500
+++ b/src/Generic.v	Fri Nov 30 11:57:55 2012 -0500
@@ -30,7 +30,7 @@
 
    Thus, to begin, we must define a syntactic representation of some class of datatypes.  In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions.
 
-   The first step is to define a representation for constructors of our datatypes. *)
+   The first step is to define a representation for constructors of our datatypes.  We use the [Record] command as a shorthand for defining an inductive type with a single constructor, plus projection functions for pulling out any of the named arguments to that constructor. *)
 
 (* EX: Define a reified representation of simple algebraic datatypes. *)
 
@@ -42,7 +42,7 @@
 
 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining.  Additionally, all of the other, non-recursive arguments can be encoded in the type [T].  When there are no non-recursive arguments, [T] can be [unit].  When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B].  We can generalize to any number of arguments via tupling.
 
-   With this definition, it as easy to define a datatype representation in terms of lists of constructors. *)
+   With this definition, it is easy to define a datatype representation in terms of lists of constructors.  The intended meaning is that the datatype came from an inductive definition including exactly the constructors in the list. *)
 
 Definition datatype := list constructor.
 

--- 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''.
 

--- a/staging/updates.rss	Wed Nov 28 19:33:21 2012 -0500
+++ b/staging/updates.rss	Fri Nov 30 11:57:55 2012 -0500
@@ -13,6 +13,14 @@
 
 <item>
         <title>Batch of changes based on proofreader feedback</title>
+        <pubDate>Fri, 30 Nov 2012 11:57:14 EST</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>Thanks to everyone who is helping with the final proofreading!</description>
+</item>
+
+<item>
+        <title>Batch of changes based on proofreader feedback</title>
         <pubDate>Sun, 11 Nov 2012 18:16:46 EST</pubDate>
         <link>http://adam.chlipala.net/cpdt/</link>
         <author>adamc@csail.mit.edu</author>