Mercurial > cpdt > repo
changeset 535:dac7a2705b00
...and back to working in 8.4 again
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 05 Aug 2015 14:57:14 -0400 |
| parents | ed829eaa91b2 |
| children | d65e9c1c9041 |
| files | src/Intro.v src/Large.v src/ProgLang.v |
| diffstat | 3 files changed, 7 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Intro.v Wed Aug 05 14:46:55 2015 -0400 +++ b/src/Intro.v Wed Aug 05 14:57:14 2015 -0400 @@ -203,7 +203,7 @@ << (custom-set-variables ... - '(coq-prog-args '("-I" "DIR/src")) + '(coq-prog-args '("-R" "DIR/src" "Cpdt")) ... ) >> @@ -211,13 +211,13 @@ 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. << -((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src"))))) +((coq-mode . ((coq-prog-args . ("-emacs-U" "-R" "DIR/src" "Cpdt"))))) >> #</li># #</ol>#%\end{enumerate}% -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. +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 <<-R DIR/src Cpdt>>. 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. 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. %\index{Proof General|)}% *)
--- a/src/Large.v Wed Aug 05 14:46:55 2015 -0400 +++ b/src/Large.v Wed Aug 05 14:57:14 2015 -0400 @@ -852,7 +852,7 @@ << (custom-set-variables ... - '(coq-prog-args '("-I" "/path/to/cpdt/src")) + '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt")) ... ) >> @@ -862,7 +862,7 @@ << (custom-set-variables ... -; '(coq-prog-args '("-I" "/path/to/cpdt/src")) +; '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt")) '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client")) ... )
--- a/src/ProgLang.v Wed Aug 05 14:46:55 2015 -0400 +++ b/src/ProgLang.v Wed Aug 05 14:57:14 2015 -0400 @@ -30,6 +30,8 @@ Ltac pl := crush; repeat (match goal with | [ |- (fun x => _) = (fun y => _) ] => ext | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal + | [ |- ?E ::: _ = ?E ::: _ ] => f_equal + | [ |- hmap _ ?E = hmap _ ?E ] => f_equal end; crush). (** At this point in the book source, some auxiliary proofs also appear. *)