# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1312382093 14400
# Node ID 690796f4690d598929b159f8569dd4edc3f87549
# Parent  f7ac1e0c0d60de29254c6bde2c14a7cdbd7bc5f3
Further emphasize necessity and purpose of Set Implicit Arguments; tweak Makefile to support parallel builds

diff -r f7ac1e0c0d60 -r 690796f4690d Makefile
--- a/Makefile	Tue Jun 28 08:38:08 2011 -0400
+++ b/Makefile	Wed Aug 03 10:34:53 2011 -0400
@@ -12,7 +12,7 @@
 .PHONY: coq clean doc dvi html templates install cpdt.tgz
 
 coq: Makefile.coq
-	make -f Makefile.coq
+	$(MAKE) -f Makefile.coq
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
@@ -21,7 +21,7 @@
 		-o Makefile.coq
 
 clean:: Makefile.coq
-	make -f Makefile.coq clean
+	$(MAKE) -f Makefile.coq clean
 	rm -f Makefile.coq .depend cpdt.tgz \
 		latex/*.sty latex/cpdt.* templates/*.v
 	rm -f *.aux *.dvi *.log
diff -r f7ac1e0c0d60 -r 690796f4690d src/StackMachine.v
--- a/src/StackMachine.v	Tue Jun 28 08:38:08 2011 -0400
+++ b/src/StackMachine.v	Wed Aug 03 10:34:53 2011 -0400
@@ -21,7 +21,7 @@
 
 (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  This chapter is not meant to give full explanations of the features that are employed.  Rather, it is meant more as an advertisement of what is possible.  Later chapters will introduce all of the concepts in bottom-up fashion.
 
-I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.2pl2 and 8.3pl1, though parts may work with other versions.
+I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.2pl2 and 8.3pl2, though parts may work with other versions.
 
 To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
 
@@ -44,7 +44,7 @@
 
 #</ol>#%\end{enumerate}%
 
-As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines [Require Import Arith Bool List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source.  In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented.  Also, be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I DIR/src#</tt>#%}%.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
+As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines [Require Import Arith Bool List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source.  In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented.  To be more specific, every chapter begins with some imports of other modules, followed by [Set Implicit Arguments.], where the latter affects the default behavior of definitions regarding type inference.  Also, be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I DIR/src#</tt>#%}%.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
 
 With Proof General, the portion of a buffer that Coq has processed is highlighted in some way, like being given a blue background.  You step through Coq source files by positioning the point at the position you want Coq to run to and pressing C-C C-RET.  This can be used both for normal step-by-step coding, by placing the point inside some command past the end of the highlighted region; and for undoing, by placing the point inside the highlighted region. *)