# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1230905375 18000
# Node ID a2b14ba218a7c2ba2845b2ff8014f858476cdafb
# Parent  df289eb8ef766da664e9d36f7e7b64b8d100c584
Typo reported by mulhern; stop publishing to Harvard

diff -r df289eb8ef76 -r a2b14ba218a7 Makefile
--- a/Makefile	Fri Jan 02 08:57:25 2009 -0500
+++ b/Makefile	Fri Jan 02 09:09:35 2009 -0500
@@ -63,5 +63,5 @@
 	cp cpdt.tgz staging/
 	cp latex/cpdt.pdf staging/
 	cp -R html staging/
-	rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/
+#	rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/
 	rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/
diff -r df289eb8ef76 -r a2b14ba218a7 src/InductiveTypes.v
--- a/src/InductiveTypes.v	Fri Jan 02 08:57:25 2009 -0500
+++ b/src/InductiveTypes.v	Fri Jan 02 09:09:35 2009 -0500
@@ -1137,7 +1137,7 @@
 
 (** %\begin{enumerate}%#<ol>#
 
-%\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe].  [Yes] stands for certain truth, [False] for certain falsehood, and [Maybe] for an unknown situation.  Define "not," "and," and "or" for this replacement boolean algebra.  Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li>#
+%\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe].  [Yes] stands for certain truth, [No] for certain falsehood, and [Maybe] for an unknown situation.  Define "not," "and," and "or" for this replacement boolean algebra.  Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li>#
 
 %\item%#<li># Modify the first example language of Chapter 2 to include variables, where variables are represented with [nat].  Extend the syntax and semantics of expressions to accommodate the change.  Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable.  Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant.  Prove that constant folding preserves the meanings of expressions.#</li>#