Merge PR #11601: [refman] Move chapters into new structure.

Reviewed-by: jfehrle

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