releases/ProofGeneral/coq/README

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.

README,v 9.1 2008/01/31 23:08:31 da Exp

Click here to go back to the front page.

Web pages by David Aspinall.
Contact Proof General maintainer.
Last modified 12 November 2009.