blob: 556273699764774d3d92c8e5dc0b5670438659a0 (
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
|
==========================
The Coq Reference Manual
==========================
------------
Introduction
------------
.. include:: introduction.rst
.. include:: license.rst
.. [#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).
.. include:: history.rst
.. include:: changes.rst
------------
The language
------------
.. toctree::
language/gallina-specification-language
language/gallina-extensions
language/coq-library
language/cic
language/module-system
----------------
The proof engine
----------------
.. toctree::
proof-engine/vernacular-commands
proof-engine/proof-handling
proof-engine/tactics
proof-engine/ltac
proof-engine/ltac2
proof-engine/detailed-tactic-examples
proof-engine/ssreflect-proof-language
---------------
User extensions
---------------
.. toctree::
user-extensions/syntax-extensions
user-extensions/proof-schemes
---------------
Practical tools
---------------
.. toctree::
practical-tools/coq-commands
practical-tools/utilities
practical-tools/coqide
--------
Addendum
--------
.. toctree::
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
addendum/sprop
.. toctree::
zebibliography
|
