.. 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).