blob: 832e6167c0ecedacb4411c8e545e5e0174b6d030 (
plain)
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
|
You can get the whole documentation of Coq in the tar file all-ps-docs.tar.
You can also get separately each document. The documentation of Coq
V6.3.1 is divided into the following documents :
* Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
* Reference-Manual-base.ps: 215 pp., includes
- the description of Gallina, the language of Coq
- the description of the Vernacular, the commands of Coq
- the description of each tactic
- chapters about Grammar/Syntax extentions and Writing tactics
- index on tactics, commands and error messages
* Reference-Manual-addendum.ps, 75 pp., includes more detailed
explanations and examples about the following topics:
- the extended Cases (C.Cornes)
- the Coercions (A. Saïbi)
- the tactic Omega (P. Crégut)
- printing proofs in natural language (Y. Coscoy)
- the tactic Ring (S. Boutin and P. Loiseleur)
- the Program tactic (C. Parent)
- the Correctness tactic (J.-C. Filliâtre)
- the extraction features (J.-C. Filliâtre)
Index, page and chapter numbers are shared by the two documents, in
order to make cross-references possible. There is also a on the ftp
server a Postscript file Reference-Manual-all.ps that contains the two
documents (base and addendum).
* Library.ps: A description of the Coq standard library;
* Changes.ps: A description of the differences between the
versions V6.3 and V6.3.1;
* rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
Documentation is also available in the DVI format (you can get the DVI docs
separately or in the tar file all-dvi.docs.tar).
The Reference Manual and the Tutorial are also available in HTML format
(online at http://coq.inria.fr or by ftp in the file doc-html.tar.gz).
|
