diff options
Diffstat (limited to 'doc/sphinx/using/libraries')
| -rw-r--r-- | doc/sphinx/using/libraries/index.rst | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst new file mode 100644 index 0000000000..d0848e6c3f --- /dev/null +++ b/doc/sphinx/using/libraries/index.rst @@ -0,0 +1,24 @@ +.. _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 |