1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
Coq Proof General
Originally written by Healfdene Goguen.
Later contributions by Patrick Loiseleur, Pierre Courtieu,
David Aspinall
Status: supported
Maintainer: Pierre Courtieu
=Coq version: 6.3, 6.3.1, 7.x, 8.0
Coq homepage: http://coq.inria.fr/
===========================================================================
Coq Proof General has experimental multiple file handling for some
versions. It does not have support for proof by pointing.
There is 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$
|