diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-05-06 16:38:03 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-05-06 16:38:03 +0000 |
| commit | 54c9e82a2ad7623191f54c914c8c0ecc26b38613 (patch) | |
| tree | 716647110baf61a20ac268cac07f18c03ff1a20c /INSTALL | |
| parent | b0045534e0197874dea3dbd8673ad0e2940c08cc (diff) | |
Added comments about info file and default values in coq.el.
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 13 |
1 files changed, 8 insertions, 5 deletions
@@ -1,3 +1,11 @@ +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 @@ -5,11 +13,6 @@ them using `byte-compile-file' in xemacs: 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 |