# HG changeset patch # User Adam Chlipala # Date 1354295446 18000 # Node ID e3b32a87347fadd1dc6fd84bf40c3579c9ea6fe0 # Parent c4a22c9ff0903f1564f6518e2dfd5e9c238f3242 Web page update on proofreading diff -r c4a22c9ff090 -r e3b32a87347f staging/index.html --- a/staging/index.html Fri Nov 30 12:07:46 2012 -0500 +++ b/staging/index.html Fri Nov 30 12:10:46 2012 -0500 @@ -40,7 +40,7 @@

Status

-

Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, then again on January 14, 2011 to support Coq 8.3, and then again on March 29, 2012 to support Coq 8.4 beta. On August 25, 2011, I started passes through all chapters, with an eye toward getting ready both for my fall class and publication by MIT Press. I'm adding bibliographic references and index entries, along with the usual tweaks and improvements.

+

Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, then again on January 14, 2011 to support Coq 8.3, and then again on March 29, 2012 to support Coq 8.4 beta. On August 25, 2011, I started passes through all chapters, with an eye toward getting ready both for my fall class and publication by MIT Press. I added bibliographic references and index entries, along with the usual tweaks and improvements. In late Summer 2012, the mode switched to final proofreading by others.

The current version is effectively a beta release. It is intended to be consistent, self-contained, and useful, both for individual study and for introductory theorem-proving classes aimed at students with ML or Haskell experience and with basic familiarity with programming language theory.