==========================
 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