# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1230904645 18000
# Node ID df289eb8ef766da664e9d36f7e7b64b8d100c584
# Parent  cadeb49dc1ef4eb2d60034d32084d82aa646a424
Small fixes while reading student solutions

diff -r cadeb49dc1ef -r df289eb8ef76 src/Coinductive.v
--- 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}% *)
diff -r cadeb49dc1ef -r df289eb8ef76 src/Extensional.v
--- 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}% *)
diff -r cadeb49dc1ef -r df289eb8ef76 src/Tactics.v
--- 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 :=