Coq Proof General

Originally written by  Healfdene Goguen.
Later contributions by Patrick Loiseleur, Pierre Courtieu, 
		       David Aspinall

Status:		supported
Maintainer:	Pierre Courtieu
Coq version:	8.0, 8.1
Coq homepage:	http://coq.inria.fr/

===========================================================================

Coq Proof General has support for X Symbol, using simple character
sequences rather than a special language of tokens (which works well
with V8's new syntax!).  See notes below.

There is a tags program, coqtags.

There is a menu option for running Coq V8 in compatibility mode
(i.e. with the -translate flag), see Coq -> Settings.

===========================================================================

Installation notes:

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.

Install coqtags in a standard place or add <proof-home>/coq to your PATH.
NB: You may need to change the path to perl at the top of the file.

Generate a TAGS file for the library by running
	coqtags `find . -name \*.v -print`
in the root directory of the library, $COQTOP/theories.  


===========================================================================

Grammar for x-symbols:

  Symbols include sequences naming Greek letters ("Lambda", "lambda", etc),
  connectives /\, \/, etc.  See the X-Symbol char table for details.

  a symbol is encoded only if 
   - preceded by _ or ' or some space or some symbol
  **and**
   - followed by _ or ' or some space or some symbol

  Grammar for sub/superscript: 

   - a double _ introduces a subscript that ends at the first space
   - a double ^ introduces a superscript that ends at the first space
  
   - a , followed by { introduces a subscript expression that ends at
     the first } (_{...} was not possible due to coq notation mechanism)

   - a ^ followed by { introduces a superscript expression that ends
     at the first }

	See example-x-symbols.v in this directory for examples.

========================================

$Id$