Mercurial > cpdt > repo
comparison src/Large.v @ 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 | f874c163f5e0 |
comparison
equal
deleted
inserted
replaced
534:ed829eaa91b2 | 535:dac7a2705b00 |
---|---|
850 The remaining ingredient is the proper way of editing library code files in Proof General. Recall this snippet of <<.emacs>> code from Chapter 2, which tells Proof General where to find the library associated with this book. | 850 The remaining ingredient is the proper way of editing library code files in Proof General. Recall this snippet of <<.emacs>> code from Chapter 2, which tells Proof General where to find the library associated with this book. |
851 | 851 |
852 << | 852 << |
853 (custom-set-variables | 853 (custom-set-variables |
854 ... | 854 ... |
855 '(coq-prog-args '("-I" "/path/to/cpdt/src")) | 855 '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt")) |
856 ... | 856 ... |
857 ) | 857 ) |
858 >> | 858 >> |
859 | 859 |
860 To do interactive editing of our current example, we just need to change the flags to point to the right places. | 860 To do interactive editing of our current example, we just need to change the flags to point to the right places. |
861 | 861 |
862 << | 862 << |
863 (custom-set-variables | 863 (custom-set-variables |
864 ... | 864 ... |
865 ; '(coq-prog-args '("-I" "/path/to/cpdt/src")) | 865 ; '(coq-prog-args '("-R" "/path/to/cpdt/src" "Cpdt")) |
866 '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client")) | 866 '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client")) |
867 ... | 867 ... |
868 ) | 868 ) |
869 >> | 869 >> |
870 | 870 |