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