--- a/latex/cpdt.tex	Tue Jan 08 16:20:01 2013 -0500
+++ b/latex/cpdt.tex	Fri Jan 18 13:45:00 2013 -0500
@@ -23,7 +23,7 @@
 \mbox{}\vfill
 \begin{center}
 
-Copyright Adam Chlipala 2008-2012.
+Copyright Adam Chlipala 2008-2013.
 
 
 This work is licensed under a

--- a/src/Intro.v	Tue Jan 08 16:20:01 2013 -0500
+++ b/src/Intro.v	Fri Jan 18 13:45:00 2013 -0500
@@ -75,7 +75,7 @@
 (** ** Dependent Types *)
 
 (**
-A language with _dependent types_ may include references to programs inside of types.  For instance, the type of an array might include a program expression giving the size of the array, making it possible to verify absence of out-of-bounds accesses statically.  Dependent types can go even further than this, effectively capturing any correctness property in a type.  For instance, later in this book, we will see how to give a Mini-ML compiler a type that guarantees that it maps well-typed source programs to well-typed target programs.
+A language with _dependent types_ may include references to programs inside of types.  For instance, the type of an array might include a program expression giving the size of the array, making it possible to verify absence of out-of-bounds accesses statically.  Dependent types can go even further than this, effectively capturing any correctness property in a type.  For instance, later in this book, we will see how to give a compiler a type that guarantees that it maps well-typed source programs to well-typed target programs.
 
 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright.  Each of %\index{PVS}%PVS and %\index{Twelf}%Twelf supports a different strict subset of Coq's dependent type language.  Twelf's type language is restricted to a bare-bones, monomorphic lambda calculus, which places serious restrictions on how complicated _computations inside types_ can be.  This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs.
 
@@ -188,7 +188,7 @@
 (**
 At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.4 and 8.4pl1.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
 
-%\index{Proof General|(}%To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
+%\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.
 
 %\begin{enumerate}%#<ol>#
 
@@ -197,7 +197,7 @@
 
 %\item %#<li>#Unpack the tarball to some directory <<DIR>>.#</li>#
 
-%\item %#<li>#Run <<make>> in <<DIR>>.#</li>#
+%\item %#<li>#Run <<make>> in <<DIR>> (ideally with a <<-j>> flag to use multiple processor cores, if you have them).#</li>#
 
 %\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the <<coqtop>> program, which provides the interactive Coq toplevel.  One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}%<<.emacs>> file, like this:
 <<

--- a/src/Large.v	Tue Jan 08 16:20:01 2013 -0500
+++ b/src/Large.v	Fri Jan 18 13:45:00 2013 -0500
@@ -217,7 +217,7 @@
 Qed.
 (* end thide *)
 
-(** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else.  I claim that step-by-step formal proofs are a poor way of conveying information.  Thus, we had might as well cut out the steps and automate as much as possible.
+(** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else.  I claim that step-by-step formal proofs are a poor way of conveying information.  Thus, we might as well cut out the steps and automate as much as possible.
 
    What about the illustrative value of proofs?  Most informal proofs are read to convey the big ideas of proofs.  How can reading [induction e; crush] convey any big ideas?  My position is that any ideas that standard automation can find are not very big after all, and the _real_ big ideas should be expressed through lemmas that are added as hints.