CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE
==================================================

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.

Versions >= 3.7 of ProofGeneral support this extension.

- 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-4.2/generic/proof-site.el" )
  - under Windows+Cygwin:
	(load-file
    "C:\\<my-pg-location>\\ProofGeneral-4.2\\generic\\proof-site.el")
where <my-pg-location> is the location of your own ProofGeneral
directory.

- 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.

Coq sources have a .v extension. Opening any .v file should
automatically launch ProofGeneral. Try this on a foo.v file.

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>/ssrcoq
or
	<my-ssreflect-location>\\ssrcoq
for Windows+Cygwin users, where <my-ssreflect-location> is the
location of the ssrcoq binary.