Mercurial > cpdt > repo

comparison src/Intro.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 686cf945dd02
children a0c604da96d3
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
209 ) 209 )
210 >> 210 >>
211 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 <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time. 211 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 <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time.
212 212
213 Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply. Here is an example that could be written in such a file to enable use of the book source. Note the need to include an argument that starts Coq in Emacs support mode. 213 Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply. Here is an example that could be written in such a file to enable use of the book source. Note the need to include an argument that starts Coq in Emacs support mode.
214 %\begin{verbatim}%#<pre>#((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))#</pre>#%\end{verbatim}% 214 <<
215 ((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))
216 >>
215 #</li># 217 #</li>#
216 218
217 #</ol>#%\end{enumerate}% 219 #</ol>#%\end{enumerate}%
218 220
219 Every chapter of this book is generated from a commented Coq source file. You can load these files and run through them step-by-step in Proof General. Be sure to run the Coq binary <<coqtop>> with the command-line argument <<-I DIR/src>>. If you have installed Proof General properly, the Coq mode should start automatically when you visit a <<.v>> buffer in Emacs, and the above advice on <<.emacs>> settings should ensure that the proper arguments are passed to <<coqtop>> by Emacs. 221 Every chapter of this book is generated from a commented Coq source file. You can load these files and run through them step-by-step in Proof General. Be sure to run the Coq binary <<coqtop>> with the command-line argument <<-I DIR/src>>. If you have installed Proof General properly, the Coq mode should start automatically when you visit a <<.v>> buffer in Emacs, and the above advice on <<.emacs>> settings should ensure that the proper arguments are passed to <<coqtop>> by Emacs.