--- a/src/Coinductive.v	Mon Dec 01 08:32:20 2008 -0500
+++ b/src/Coinductive.v	Fri Jan 02 08:57:25 2009 -0500
@@ -467,7 +467,7 @@
   %\item%#<li># Define a function [map] for building an output tree out of two input trees by traversing them in parallel and applying a two-argument function to their corresponding data values.#</li>#
   %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
   %\item%#<li># Define a tree [true_false] where the root node has value [true], its children have value [false], all nodes at the next have the value [true], and so on, alternating boolean values from level to level.#</li>#
-  %\item%#<li># Prove that [true_falses] is equal to the result of mapping the boolean "or" function [orb] over [true_false] and [falses].  You can make [orb] available with [Require Import Bool.].  You may find the lemma [orb_false_r] from the same module helpful.  Your proof here should not be about the standard equality [=], but rather about some new equality relation that you define.#</li>#
+  %\item%#<li># Prove that [true_false] is equal to the result of mapping the boolean "or" function [orb] over [true_false] and [falses].  You can make [orb] available with [Require Import Bool.].  You may find the lemma [orb_false_r] from the same module helpful.  Your proof here should not be about the standard equality [=], but rather about some new equality relation that you define.#</li>#
 #</ol>#%\end{enumerate}% #</li>#
 
 #</ol>#%\end{enumerate}% *)

--- a/src/Extensional.v	Mon Dec 01 08:32:20 2008 -0500
+++ b/src/Extensional.v	Fri Jan 02 08:57:25 2009 -0500
@@ -1013,7 +1013,7 @@
 
   It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type.  This is not as big of a problem as it seems.  For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
 
-  For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr].  Also extend the correctness theorem to apply to your new definition.  You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter.
+  For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr].  Also extend the correctness theorem to apply to your new definition.  You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter.  Any such axiom should only mention syntax; it should not mention any compilation or denotation functions.  Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem.
  #</li>#
    
 #</ol>#%\end{enumerate}% *)

--- a/src/Tactics.v	Mon Dec 01 08:32:20 2008 -0500
+++ b/src/Tactics.v	Fri Jan 02 08:57:25 2009 -0500
@@ -137,13 +137,13 @@
 
 Ltac crush := crush' false fail.
 
-Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
+Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),
   (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
                                                | refl_equal => v'
                                              end))
   -> P v.
   intros.
-  generalize (H _ v (refl_equal _)); trivial.
+  generalize (X _ v (refl_equal _)); trivial.
 Qed.
 
 Ltac dep_destruct E :=