.. _introduction:

.. include:: preamble.rst
.. include:: replaces.rst

Introduction
===========================================

.. include:: introduction.rst
.. include:: credits.rst

------------------
Table of contents
------------------

.. toctree::
   :caption: The language

   language/gallina-extensions
   language/coq-library
   language/cic
   language/module-system

.. toctree::
   :caption: The proof engine

   proof-engine/tactics
   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/coqide

.. toctree::
   :caption: Addendum

   addendum/extended-pattern-matching
   addendum/canonical-structures
   addendum/omega
   addendum/micromega

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