blob: 0bd3054788a73cd2f09b87836ca58f405c3ec2a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
.. _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
|
