Restaured the config files (including doc) for PG in the ssreflect package.

2 files changed, 86 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/INSTALL.pg b/mathcomp/ssreflect/INSTALL.pg
new file mode 100644
index 0000000..5b02e57
--- /dev/null
+++ b/mathcomp/ssreflect/INSTALL.pg
@@ -0,0 +1,40 @@
+
+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.
+
+The >= 3.7 versions 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:
+  - under Unix/MacOS:
+	(load-file
+    "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
+  - under Windows+Cygwin:
+	(load-file
+    "C:\\<my-pg-location>\\ProofGeneral-3.7\\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:
+	(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.
+
+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:
+	'Advanced/Customize/Coq/Coq Prog Name' Change the value of the
+variable to
+	 <my-ssreflect-location>/bin/ssrcoq
+or
+	<my-ssreflect-location>\\bin\\ssrcoq
+for Windows+Cygwin users, where <my-ssreflect-location> is the location of
+your coq directory.
diff --git a/mathcomp/ssreflect/pg-ssr.el b/mathcomp/ssreflect/pg-ssr.el
new file mode 100644
index 0000000..a2a36fd
--- /dev/null
+++ b/mathcomp/ssreflect/pg-ssr.el
@@ -0,0 +1,46 @@
+;; Customization of PG for ssreflect syntax
+;; Assia Mahboubi 2007
+
+(defcustom coq-user-tactics-db
+   '(("nat_congr" "ncongr"  "nat_congr" t "nat_congr")
+     ("nat_norm" "nnorm"  "nat_norm" t "nat_norm")
+     ("bool_congr" "bcongr"  "bool_congr" t "bool_congr")
+     ("prop_congr" "prcongr"  "prop_congr" t "prop_congr")
+     ("move" "m"  "move" t "move")
+     ("set" "set"  "set # := #" t "set")
+     ("have" "hv" "have # : #" t "have")
+     ("congr" "con" "congr #" t "congr")
+     ("wlog" "wlog" "wlog : / #" t "wlog")
+     ("without loss" "wilog" "without loss #" t "without loss")
+     ("unlock" "unlock" "unlock #" t "unlock")
+     ("suffices" "suffices" "suffices # : #" t "suffices")
+     ("suff" "suff" "suff # : #" t "suff")
+)
+   "Extended list of tactics, includings ssr and user defined ones")
+
+
+(defcustom coq-user-commands-db
+  '(("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits")
+    ("Hint View for" "hv" "Hint View for #" t "Hint\\s-+View\\s-+for")
+    ("inside" "ins" nil f "inside")
+    ("outside" "outs" nil f "outside")
+    ("Canonical " nil "Canonical  #." t "Canonical")
+)
+   "Extended list of commands, includings ssr and user defined ones")
+
+(defcustom coq-user-tacticals-db
+  '(("last" "lst" nil t "last"))
+  "Extended list of tacticals, includings ssr and user defined ones")
+
+(defcustom coq-user-reserved-db
+  '("is" "nosimpl" "of")
+  "Extended list of keywords, includings ssr and user defined ones")
+
+(defcustom coq-user-solve-tactics-db
+  '(("done" nil "done" nil "done")
+    )
+   "Extended list of closing tactic(al)s, includings ssr and user defined ones")
+;; This works only with the cvs version (> 3.7) of Proof General.
+(defcustom coq-variable-highlight-enable nil
+  "Activates partial bound variable highlighting"
+)