aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--INSTALL13
1 files changed, 8 insertions, 5 deletions
diff --git a/INSTALL b/INSTALL
index 8771d108..10881ad8 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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