blob: baf2e0d9819ee1c2031c6a0122f165e00f4599be (
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
.. include:: preamble.rst
.. include:: replaces.rst
.. include:: introduction.rst
------------------
Table of contents
------------------
.. toctree::
:caption: Indexes
genindex
coq-cmdindex
coq-tacindex
coq-optindex
coq-exnindex
.. No entries yet
* :index:`thmindex`
.. toctree::
:caption: Preamble
self
credits
.. toctree::
:caption: The language
language/gallina-specification-language
language/gallina-extensions
language/coq-library
language/cic
language/module-system
.. toctree::
:caption: The proof engine
proof-engine/vernacular-commands
proof-engine/proof-handling
proof-engine/tactics
proof-engine/ltac
proof-engine/detailed-tactic-examples
proof-engine/ssreflect-proof-language
.. toctree::
:caption: User extensions
user-extensions/syntax-extensions
user-extensions/proof-schemes
.. toctree::
:caption: Practical tools
practical-tools/coq-commands
practical-tools/utilities
practical-tools/coqide
.. toctree::
:caption: Addendum
addendum/extended-pattern-matching
addendum/implicit-coercions
addendum/canonical-structures
addendum/type-classes
addendum/omega
addendum/micromega
addendum/extraction
addendum/program
addendum/ring
addendum/nsatz
addendum/generalized-rewriting
addendum/parallel-proof-processing
addendum/miscellaneous-extensions
addendum/universe-polymorphism
.. toctree::
:caption: Reference
zebibliography
This material (the Coq Reference Manual) may be distributed only subject to the
terms and conditions set forth in the Open Publication License, v1.0 or later
(the latest version is presently available at
http://www.opencontent.org/openpub). Options A and B are not elected.
.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
Optionally, you can enhance it with the minor mode
Company-Coq :cite:`Pit16`
(see https://github.com/cpitclaudel/company-coq).
|
