# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223391036 14400
# Node ID 9b0d118abbc9e3add395fcbd7bb988744514d52e
# Parent  939add5a7db98ae0817aa761cd551c376cce7082
Remove -impredicative-set from text

diff -r 939add5a7db9 -r 9b0d118abbc9 src/StackMachine.v
--- a/src/StackMachine.v	Tue Oct 07 10:49:07 2008 -0400
+++ b/src/StackMachine.v	Tue Oct 07 10:50:36 2008 -0400
@@ -26,7 +26,7 @@
 There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% program.  The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\texttt{%#<tt>#.emacs#</tt>#%}% file, like this:
 %\begin{verbatim}%#<pre>#(custom-set-variables
   ...
-  '(coq-prog-args '("-impredicative-set" "-I" "/path/to/cpdt/src"))
+  '(coq-prog-args '("-I" "/path/to/cpdt/src"))
   ...
 )#</pre>#%\end{verbatim}%
 The extra arguments demonstrated here are the proper choices for working with the code for this book.  The ellipses stand for other Emacs customization settings you may already have.  It can be helpful to save several alternate sets of flags in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, with all but one commented out within the %\texttt{%#<tt>#custom-set-variables#</tt>#%}% block at any given time.