blob: f5a57b9dd0f669f8655a203221d5fc6fb8c8dacc (
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
|
.. _introduction:
.. include:: preamble.rst
.. include:: replaces.rst
Introduction
===========================================
.. include:: introduction.rst
.. include:: credits.rst
------------------
Table of contents
------------------
.. toctree::
:caption: The language
.. toctree::
:caption: The proof engine
.. toctree::
:caption: User extensions
.. toctree::
:caption: Practical tools
.. toctree::
:caption: Addendum
.. toctree::
:caption: Reference
zebibliography
.. toctree::
:caption: Indexes
genindex
coq-cmdindex
coq-tacindex
coq-optindex
coq-exnindex
.. No entries yet
* :index:`thmindex`
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.
|
