blob: 0a20d1c47bfb084f4f59e376775b1dc76f666ddf (
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
|
==========================
Introduction and Contents
==========================
.. include:: introduction.rst
Contents
--------
.. toctree::
:caption: Indexes
genindex
coq-cmdindex
coq-tacindex
coq-optindex
coq-exnindex
.. No entries yet
* :index:`thmindex`
.. toctree::
:caption: Preamble
self
history
changes
.. 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/ltac2
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
addendum/sprop
.. toctree::
:caption: Reference
zebibliography
.. 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).
|
