INSTALL


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

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.

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.

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)