# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1258396054 18000
# Node ID 9d0b9577f8b159ebbc4e0aa065262e3e24e0b930
# Parent  19902d0b662251805eecde6af3599c41f8da82e2
First 8.2 release

diff -r 19902d0b6622 -r 9d0b9577f8b1 Makefile
--- a/Makefile	Mon Nov 16 13:13:34 2009 -0500
+++ b/Makefile	Mon Nov 16 13:27:34 2009 -0500
@@ -45,7 +45,7 @@
 	cd latex ; latex $* ; latex $*
 
 latex/%.pdf: latex/%.dvi
-	cd latex ; pdflatex $*
+	cd latex ; pdflatex $* ; pdflatex $*
 
 html: Makefile $(VS) src/toc.html
 	mkdir -p html
@@ -68,5 +68,4 @@
 	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/* ssh.hcoop.net:sites/chlipala/adam/cpdt/
+	rsync -az --exclude '*~' staging/* schizomaniac.net:sites/chlipala/adam/cpdt/
diff -r 19902d0b6622 -r 9d0b9577f8b1 src/toc.html
--- a/src/toc.html	Mon Nov 16 13:13:34 2009 -0500
+++ b/src/toc.html	Mon Nov 16 13:27:34 2009 -0500
@@ -13,6 +13,7 @@
 <li><a href="MoreDep.html">More Dependent Types</a>
 <li><a href="DataStruct.html">Dependent Data Structures</a>
 <li><a href="Equality.html">Reasoning About Equality Proofs</a>
+<li><a href="Generic.html">Generic Programming</a>
 <li><a href="Match.html">Proof Search in Ltac</a>
 <li><a href="Reflection.html">Proof by Reflection</a>
 <li><a href="Firstorder.html">First-Order Abstract Syntax</a>
@@ -21,6 +22,5 @@
 <li><a href="Extensional.html">Extensional Transformations</a>
 <li><a href="Intensional.html">Intensional Transformations</a>
 <li><a href="Impure.html">Modeling Impure Languages</a>
-<li><a href="Generic.html">Generic Programming</a>
 
 </body></html>
diff -r 19902d0b6622 -r 9d0b9577f8b1 staging/index.html
--- a/staging/index.html	Mon Nov 16 13:13:34 2009 -0500
+++ b/staging/index.html	Mon Nov 16 13:27:34 2009 -0500
@@ -8,15 +8,28 @@
 
 <div class="summary">
 <p>This is the web site for an in-progress textbook about practical engineering with <a href="http://coq.inria.fr/">the Coq proof assistant</a>.  The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p>
-
-<p>This is the text for a <a href="http://www.cs.harvard.edu/~adamc/cpdt/">Fall 2008 class at Harvard</a>.</p>
 </div>
 
 <div class="project">
+<h2>Distribution Formats</h2>
 <ul>
 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li>
 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
+</ul>
+</div>
+
+<div class="project">
+<h2>Used by:</h2>
+<ul>
+<li> CS252 at Harvard <a href="http://www.cs.harvard.edu/~adamc/cpdt/">(Fall 2008)</a></li>
+</ul>
+</div>
+
+<div class="project">
+<h2>Status</h2>
+
+<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1.  Some chapters on programming languages and compilers are empty or just contain Coq code; these should be filled in soon-ish.  Additional plans: a chapter on (practical aspects of) CIC metatheory and axioms; a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax; more examples of Ltac design patterns; discussion of tactic debugging and maintenance.</p>
 </div>
 
 </body></html>