Small updates in the documentation of the customization of PG.

1 files changed, 25 insertions, 17 deletions

diff --git a/mathcomp/ssreflect/INSTALL.pg b/mathcomp/ssreflect/INSTALL.pg
index 5b02e57..e4305fc 100644
--- a/mathcomp/ssreflect/INSTALL.pg
+++ b/mathcomp/ssreflect/INSTALL.pg
@@ -2,27 +2,30 @@
 CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE
 ==================================================
 
-The ssreflect distribution comes with a small configuration file
-pg-ssr.el to extend ProofGeneral (PG), a generic interface for
-proof assistants based on the customizable text editor Emacs, to the
-syntax of ssreflect.
+ProofGeneral (PG) is a generic interface for proof assistants based on
+the customizable text editor Emacs. The ssreflect distribution includes
+a small configuration file, pg-ssr.el, which allows to extend PG's
+syntax highlighting features to the syntax of the ssreflect extension
+of Coq's tactic language.
 
-The >= 3.7 versions of ProofGeneral support this extension.
+Versions >= 3.7 of ProofGeneral support this extension.
 
-- Following the installation instructions, unpack the sources of PG in
-a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add
-the following line to your .emacs file:
+- Follow the installation instructions of PG (see
+  http://proofgeneral.inf.ed.ac.uk/), and unpack the sources of PG in
+a directory, for instance <my-pg-location>/ProofGeneral-4.2.
+
+- Add the following line to your .emacs configuration file:
   - under Unix/MacOS:
 	(load-file
-    "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
+    "<my-pg-location>/ProofGeneral-4.2/generic/proof-site.el" )
   - under Windows+Cygwin:
 	(load-file
-    "C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el")
+    "C:\\<my-pg-location>\\ProofGeneral-4.2\\generic\\proof-site.el")
 where <my-pg-location> is the location of your own ProofGeneral
 directory.
 
--Immediately after the previous line added to your .emacs, add this
-one:
+- Add the following line to your .emacs configuration file (after the
+  previous one):
 	(load-file "<my-pgssr-location>/pg-ssr.el") respectively
 	(load-file "<my-pgssr-location>\\pg-ssr.el") for Windows+Cygwin
 users, where <my-pgssr-location> is the location of your pg-ssr.el file.
@@ -30,11 +33,16 @@ users, where <my-pgssr-location> is the location of your pg-ssr.el file.
 Coq sources have a .v extension. Opening any .v file should
 automatically launch ProofGeneral. Try this on a foo.v file.
 
-In the menu 'ProofGeneral', choose the item:
+In case you are linking the code of the ssreflect extension statically
+(this is not the default situation, and not the recommended option),
+then the executable Coq top level which includes the ssreflect
+extension is called 'ssrcoq'. In order to use it in PG:
+
+- In the menu 'ProofGeneral', choose the item:
 	'Advanced/Customize/Coq/Coq Prog Name' Change the value of the
 variable to
-	 <my-ssreflect-location>/bin/ssrcoq
+	 <my-ssreflect-location>/ssrcoq
 or
-	<my-ssreflect-location>\\bin\\ssrcoq
-for Windows+Cygwin users, where <my-ssreflect-location> is the location of
-your coq directory.
+	<my-ssreflect-location>\\ssrcoq
+for Windows+Cygwin users, where <my-ssreflect-location> is the
+location of the ssrcoq binary.