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