.. _libraries:

=====================
Libraries and plugins
=====================

Coq is distributed with a standard library and a set of internal
plugins (most of which provide tactics that have already been
presented in :ref:`writing-proofs`).  This chapter presents this
standard library and some of these internal plugins which provide
features that are not tactics.

In addition, Coq has a rich ecosystem of external libraries and
plugins.  These libraries and plugins can be browsed online through
the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and
installed with the `opam package manager
<https://coq.inria.fr/opam-using.html>`_.

.. toctree::
   :maxdepth: 1

   ../../language/coq-library
   ../../addendum/extraction
   ../../addendum/miscellaneous-extensions
   funind
   writing