[refman] Move chapters into new structure.

As a first step toward a deeper refactoring of the reference manual,
we move existing chapters into a new structure.

We use the Sphinx support for top-level chapters spanning multiple
pages to consolidate existing chapters into a smaller number of
chapters and a smaller number of parts.

Now the full top-level table of content can be seen in one glance.
Most of the new chapters are divided into several sub-chapters (on
separate pages) that correspond to the pre-existing chapters.  These
new top-level chapters gathering several chapters together have gained
a new introduction.  The main introduction has been rewritten /
simplified as well.

For now, the URL of pre-existing chapters does not change.  The intent
is to further refactor the manual by splitting some of these
sub-chapters into smaller ones, and by moving things around.

While the sub-chapters are likely to evolve very much in the future,
the top-level table of content is almost final (except that the "Using
Coq" part may gain one or two additional chapters on proof engineering
/ project management).

Thanks to Jim Fehrle for investigating how to split a chapter on
multiple pages and to both Jim and Matthieu Sozeau for the discussion
that led to this new structure.

See also the related CEP: https://github.com/coq/ceps/pull/43

Additional notes:

- A new directory structure has been created reflecting the new
  chapter structure.

- The indexes chapter has been removed from the PDF version since it
  wasn't working.

Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>

2 files changed, 44 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..2228df5ab8
--- /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:
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../language/coq-library
+   ../../addendum/extraction
+   ../../addendum/miscellaneous-extensions
+
+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>`_.
diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst
new file mode 100644
index 0000000000..4381c4d63d
--- /dev/null
+++ b/doc/sphinx/using/tools/index.rst
@@ -0,0 +1,20 @@
+.. _tools:
+
+================================
+Command-line and graphical tools
+================================
+
+This chapter presents the command-line tools that users will need to
+build their Coq project, the documentation of the CoqIDE standalone
+user interface and the documentation of the parallel proof processing
+feature that is supported by CoqIDE and several other user interfaces.
+A list of available user interfaces to interact with Coq is available
+on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../practical-tools/coq-commands
+   ../../practical-tools/utilities
+   ../../practical-tools/coqide
+   ../../addendum/parallel-proof-processing