blob: 10881ad81c156d096a92960d056f11d106284808 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
Put the compiled emacs files and the file script-management.info in a
suitable directory for local emacs files, as suggested by your system
administrator. Otherwise, alter the coq-info-dir in coq.el to a
hard-coded path where you put the file script-management.info.
Check the values of coq-tags and coq-prog-name in coq.el to see that
they correspond to the paths for coqtop and the library on your system.
To install, put the .el files in an appropriate directory and compile
them using `byte-compile-file' in xemacs:
M-0 M-x byte-recompile-directory
If you want to use this mode for Coq, you need to make sure you have
an appropriate version, which is from later than 1 March 1998.
Install coqtags or legotags in a standard place.
If you are running Coq, generate a TAGS file for the library by running
coqtags `find . -name \*.v -print`
in the root directory of the library, $COQTOP/theories.
Finally, you may want to add the following lines to your .emacs file:
;;; LEGO and Coq
(setq auto-mode-alist
(cons '("\\.v" . coq-mode)
(cons '("\\.l$" . lego-mode) auto-mode-alist)))
(autoload 'coq-mode "coq"
"Major mode for editing Coq vernacular." t)
(autoload 'lego-mode "lego"
"Major mode for editing Lego proof scripts." t)
; Tags is unusable with Coq library otherwise:
(setq tag-always-exact t)
|
