index.latex.rst

The Coq Reference Manual

Introduction

[1]	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).

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