[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>

16 files changed, 360 insertions, 247 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index d909f98956..41b726b069 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -1,7 +1,7 @@
 .. _extraction:
 
-Extraction of programs in |OCaml| and Haskell
-=============================================
+Program extraction
+==================
 
 :Authors: Jean-Christophe Filliâtre and Pierre Letouzey
 
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index db8c09d88f..0e8660cb0e 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -1,10 +1,5 @@
-.. _miscellaneousextensions:
-
-Miscellaneous extensions
-========================
-
 Program derivation
-------------------
+==================
 
 |Coq| comes with an extension called ``Derive``, which supports program
 derivation. Typically in the style of Bird and Meertens or derivations
diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst
new file mode 100644
index 0000000000..3535a4d8a7
--- /dev/null
+++ b/doc/sphinx/appendix/history-and-changes/index.rst
@@ -0,0 +1,20 @@
+.. _history-and-changes:
+
+==========================
+History and recent changes
+==========================
+
+This chapter is divided in two parts.  The first one is about the
+early history of Coq and is presented in chronological order.  The
+second one provides release notes about recent versions of Coq and is
+presented in reverse chronological order.  When updating your copy of
+Coq to a new version (especially a new major version), it is strongly
+recommended that you read the corresponding release notes.  They may
+contain advice that will help you understand the differences with the
+previous version and upgrade your projects.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../history
+   ../../changes
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
new file mode 100644
index 0000000000..a5032ff822
--- /dev/null
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -0,0 +1,24 @@
+:orphan:
+
+.. _indexes:
+
+========
+Indexes
+========
+
+We provide various specialized indexes that are helpful to quickly
+find what you are looking for.
+
+.. toctree::
+
+   ../../genindex
+   ../../coq-cmdindex
+   ../../coq-tacindex
+   ../../coq-optindex
+   ../../coq-exnindex
+
+For reference, here are direct links to the documentation of:
+
+- :ref:`flags, options and tables <flags-options-tables>`;
+- controlling the display of warning messages with the :opt:`Warnings`
+  option.
diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst
index 29f792b3aa..e3a27fd7c4 100644
--- a/doc/sphinx/genindex.rst
+++ b/doc/sphinx/genindex.rst
@@ -2,6 +2,6 @@
 
 .. hack to get index in TOC
 
------
-Index
------
+-------------
+General index
+-------------
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 0a20d1c47b..6069ed42fe 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -8,84 +8,37 @@ Contents
 --------
 
 .. toctree::
-   :caption: Indexes
-
-   genindex
-   coq-cmdindex
-   coq-tacindex
-   coq-optindex
-   coq-exnindex
-
-.. No entries yet
-  * :index:`thmindex`
-
-.. toctree::
-   :caption: Preamble
 
    self
-   history
-   changes
 
 .. toctree::
-   :caption: The language
+   :caption: Specification language
 
-   language/gallina-specification-language
-   language/gallina-extensions
-   language/coq-library
-   language/cic
-   language/module-system
+   language/core/index
+   language/extensions/index
 
 .. toctree::
-   :caption: The proof engine
+   :caption: Proofs
 
-   proof-engine/vernacular-commands
-   proof-engine/proof-handling
-   proof-engine/tactics
-   proof-engine/ltac
-   proof-engine/ltac2
-   proof-engine/detailed-tactic-examples
-   proof-engine/ssreflect-proof-language
+   proofs/writing-proofs/index
+   proofs/automatic-tactics/index
+   proofs/creating-tactics/index
 
 .. toctree::
-   :caption: User extensions
+   :caption: Using Coq
 
-   user-extensions/syntax-extensions
-   user-extensions/proof-schemes
+   using/libraries/index
+   using/tools/index
 
 .. toctree::
-   :caption: Practical tools
+   :caption: Appendix
 
-   practical-tools/coq-commands
-   practical-tools/utilities
-   practical-tools/coqide
-
-.. toctree::
-   :caption: Addendum
-
-   addendum/extended-pattern-matching
-   addendum/implicit-coercions
-   addendum/canonical-structures
-   addendum/type-classes
-   addendum/omega
-   addendum/micromega
-   addendum/extraction
-   addendum/program
-   addendum/ring
-   addendum/nsatz
-   addendum/generalized-rewriting
-   addendum/parallel-proof-processing
-   addendum/miscellaneous-extensions
-   addendum/universe-polymorphism
-   addendum/sprop
+   appendix/history-and-changes/index
+   appendix/indexes/index
+   zebibliography
 
-.. toctree::
-   :caption: Reference
+.. No entries yet
+  * :index:`thmindex`
 
-   zebibliography
 
 .. include:: license.rst
-
-.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
-   Optionally, you can enhance it with the minor mode
-   Company-Coq :cite:`Pit16`
-   (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 5562736997..62d9525194 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -10,81 +10,39 @@ Introduction
 
 .. include:: license.rst
 
-.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
-   Optionally, you can enhance it with the minor mode
-   Company-Coq :cite:`Pit16`
-   (see https://github.com/cpitclaudel/company-coq).
-
-.. include:: history.rst
-
-.. include:: changes.rst
-
-------------
-The language
-------------
+----------------------
+Specification language
+----------------------
 
 .. toctree::
 
-   language/gallina-specification-language
-   language/gallina-extensions
-   language/coq-library
-   language/cic
-   language/module-system
+   language/core/index
+   language/extensions/index
 
-----------------
-The proof engine
-----------------
+------
+Proofs
+------
 
 .. toctree::
 
-   proof-engine/vernacular-commands
-   proof-engine/proof-handling
-   proof-engine/tactics
-   proof-engine/ltac
-   proof-engine/ltac2
-   proof-engine/detailed-tactic-examples
-   proof-engine/ssreflect-proof-language
+   proofs/writing-proofs/index
+   proofs/automatic-tactics/index
+   proofs/creating-tactics/index
 
----------------
-User extensions
----------------
+---------
+Using Coq
+---------
 
 .. toctree::
 
-   user-extensions/syntax-extensions
-   user-extensions/proof-schemes
-
----------------
-Practical tools
----------------
-
-.. toctree::
-
-   practical-tools/coq-commands
-   practical-tools/utilities
-   practical-tools/coqide
+   using/libraries/index
+   using/tools/index
 
 --------
-Addendum
+Appendix
 --------
 
 .. toctree::
 
-   addendum/extended-pattern-matching
-   addendum/implicit-coercions
-   addendum/canonical-structures
-   addendum/type-classes
-   addendum/omega
-   addendum/micromega
-   addendum/extraction
-   addendum/program
-   addendum/ring
-   addendum/nsatz
-   addendum/generalized-rewriting
-   addendum/parallel-proof-processing
-   addendum/miscellaneous-extensions
-   addendum/universe-polymorphism
-   addendum/sprop
-
-.. toctree::
+   appendix/history-and-changes/index
    zebibliography
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 1424b4f3e1..b059fb4069 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,107 +1,68 @@
-This document is the Reference Manual of the |Coq| proof assistant.
-To start using Coq, it is advised to first read a tutorial.
-Links to several tutorials can be found at
-https://coq.inria.fr/documentation and
-https://github.com/coq/coq/wiki#coq-tutorials
-
-The |Coq| system is designed to develop mathematical proofs, and
-especially to write formal specifications, programs and to verify that
-programs are correct with respect to their specifications. It provides a
-specification language named |Gallina|. Terms of |Gallina| can represent
-programs as well as properties of these programs and proofs of these
-properties. Using the so-called *Curry-Howard isomorphism*, programs,
-properties and proofs are formalized in the same language called
-*Calculus of Inductive Constructions*, that is a
-:math:`\lambda`-calculus with a rich type system. All logical judgments
-in |Coq| are typing judgments. The very heart of the |Coq| system is the
-type checking algorithm that checks the correctness of proofs, in other
-words that checks that a program complies to its specification. |Coq| also
-provides an interactive proof assistant to build proofs using specific
-programs called *tactics*.
-
-All services of the |Coq| proof assistant are accessible by interpretation
-of a command language called *the vernacular*.
-
-Coq has an interactive mode in which commands are interpreted as the
-user types them in from the keyboard and a compiled mode where commands
-are processed from a file.
-
--  In interactive mode, users can develop their theories and proofs step by
-   step, and query the system for available theorems and definitions. The
-   interactive mode is generally run with the help of an IDE, such
-   as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`,
-   Emacs with Proof-General :cite:`Asp00` [#PG]_,
-   or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq).
-   The `coqtop` read-eval-print-loop can also be used directly, for debugging
-   purposes.
-
--  The compiled mode acts as a proof checker taking a file containing a
-   whole development in order to ensure its correctness. Moreover,
-   |Coq|’s compiler provides an output file containing a compact
-   representation of its input. The compiled mode is run with the `coqc`
-   command.
-
-.. seealso:: :ref:`thecoqcommands`.
-
-How to read this book
----------------------
-
-This is a Reference Manual, so it is not intended for continuous reading.
-We recommend using the various indexes to quickly locate the documentation
-you are looking for. There is a global index, and a number of specific indexes
-for tactics, vernacular commands, and error messages and warnings.
-Nonetheless, the manual has some structure that is explained below.
-
--  The first part describes the specification language, |Gallina|.
-   Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete
-   syntax as well as the meaning of programs, theorems and proofs in the
-   Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the
-   standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description
-   of the formalism. Chapter :ref:`themodulesystem` describes the module
-   system.
-
--  The second part describes the proof engine. It is divided into several
-   chapters. Chapter :ref:`vernacularcommands` presents all commands (we
-   call them *vernacular commands*) that are not directly related to
-   interactive proving: requests to the environment, complete or partial
-   evaluation, loading and compiling files. How to start and stop
-   proofs, do multiple proofs in parallel is explained in
-   Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that
-   realize one or more steps of the proof are presented: we call them
-   *tactics*. The legacy language to combine these tactics into complex proof
-   strategies is given in Chapter :ref:`ltac`. The currently experimental
-   language that will eventually replace Ltac is presented in
-   Chapter :ref:`ltac2`. Examples of tactics
-   are described in Chapter :ref:`detailedexamplesoftactics`.
-   Finally, the |SSR| proof language is presented in
-   Chapter :ref:`thessreflectprooflanguage`.
-
--  The third part describes how to extend the syntax of |Coq| in
-   Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define
-   new induction principles in Chapter :ref:`proofschemes`.
-
--  In the fourth part more practical tools are documented. First in
-   Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and
-   `coqtop` (interactive mode) with their options is described. Then,
-   in Chapter :ref:`utilities`, various utilities that come with the
-   |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` 
-   describes CoqIDE.
-
--  The fifth part documents a number of advanced features, including coercions,
-   canonical structures, typeclasses, program extraction, and specialized
-   solvers and tactics. See the table of contents for a complete list.
-
-List of additional documentation
---------------------------------
-
-This manual does not contain all the documentation the user may need
-about |Coq|. Various informations can be found in the following documents:
-
-Installation
-    A text file `INSTALL` that comes with the sources explains how to
-    install |Coq|.
-
-The |Coq| standard library
-    A commented version of sources of the |Coq| standard library
-    (including only the specifications, the proofs are removed) is
-    available at https://coq.inria.fr/stdlib/.
+This is the reference manual of |Coq|.  Coq is an interactive theorem
+prover.  It lets you formalize mathematical concepts and then helps
+you interactively generate machine-checked proofs of theorems.
+Machine checking gives users much more confidence that the proofs are
+correct compared to human-generated and -checked proofs.  Coq has been
+used in a number of flagship verification projects, including the
+`CompCert verified C compiler <http://compcert.inria.fr/>`_, and has
+served to verify the proof of the `four color theorem
+<https://github.com/math-comp/fourcolor>`_ (among many other
+mathematical formalizations).
+
+Users generate proofs by entering a series of tactics that constitute
+steps in the proof.  There are many built-in tactics, some of which
+are elementary, while others implement complex decision procedures
+(such as :tacn:`lia`, a decision procedure for linear integer
+arithmetic).  :ref:`Ltac <ltac>` and its planned replacement,
+:ref:`Ltac2 <ltac2>`, provide languages to define new tactics by
+combining existing tactics with looping and conditional constructs.
+These permit automation of large parts of proofs and sometimes entire
+proofs.  Furthermore, users can add novel tactics or functionality by
+creating Coq plugins using OCaml.
+
+The Coq kernel, a small part of Coq, does the final verification that
+the tactic-generated proof is valid.  Usually the tactic-generated
+proof is indeed correct, but delegating proof verification to the
+kernel means that even if a tactic is buggy, it won't be able to
+introduce an incorrect proof into the system.
+
+Finally, Coq also supports extraction of verified programs to
+programming languages such as OCaml and Haskell.  This provides a way
+of executing Coq code efficiently and can be used to create verified
+software libraries.
+
+To learn Coq, beginners are advised to first start with a tutorial /
+book.  Several such tutorials / books are listed at
+https://coq.inria.fr/documentation.
+
+This manual is organized in three main parts, plus an appendix:
+
+- **The first part presents the specification language of Coq**, that
+  allows to define programs and state mathematical theorems.
+  :ref:`core-language` presents the language that the kernel of Coq
+  understands.  :ref:`extensions` presents the richer language, with
+  notations, implicits, etc. that a user can use and which is
+  translated down to the language of the kernel by means of an
+  "elaboration process".
+
+- **The second part presents the interactive proof mode**, the central
+  feature of Coq.  :ref:`writing-proofs` introduces this interactive
+  proof mode and the available proof languages.
+  :ref:`automatic-tactics` presents some more advanced tactics, while
+  :ref:`writing-tactics` is about the languages that allow a user to
+  combine tactics together and develop new ones.
+
+- **The third part shows how to use Coq in practice.**
+  :ref:`libraries` presents some of the essential reusable blocks from
+  the ecosystem and some particularly important extensions such as the
+  program extraction mechanism.  :ref:`tools` documents important
+  tools that a user needs to build a Coq project.
+
+- In the appendix, :ref:`history-and-changes` presents the history of
+  Coq and changes in recent releases.  This is an important reference
+  if you upgrade the version of Coq that you use.  The various
+  :ref:`indexes <indexes>` are very useful to **quickly browse the
+  manual and find what you are looking for.** They are often the main
+  entry point to the manual.
+
+The full table of contents is presented below:
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
new file mode 100644
index 0000000000..c78c0737db
--- /dev/null
+++ b/doc/sphinx/language/core/index.rst
@@ -0,0 +1,39 @@
+.. _core-language:
+
+=============
+Core language
+=============
+
+At the heart of the Coq proof assistant is the Coq kernel.  While
+users have access to a language with many convenient features such as
+notations, implicit arguments, etc. (that are presented in the
+:ref:`next chapter <extensions>`), such complex terms get translated
+down to a core language (the Calculus of Inductive Constructions) that
+the kernel understands, and which we present here.  Furthermore, while
+users can build proofs interactively using tactics (see Chapter
+:ref:`writing-proofs`), the role of these tactics is to incrementally
+build a "proof term" which the kernel will verify.  More precisely, a
+proof term is a term of the Calculus of Inductive Constructions whose
+type corresponds to a theorem statement.  The kernel is a type checker
+which verifies that terms have their expected type.
+
+This separation between the kernel on the one hand and the elaboration
+engine and tactics on the other hand follows what is known as the "de
+Bruijn criterion" (keeping a small and well delimited trusted code
+base within a proof assistant which can be much more complex).  This
+separation makes it possible to reduce the trust in the whole system
+to trusting a smaller, critical component: the kernel.  In particular,
+users may rely on external plugins that provide advanced and complex
+tactics without fear of these tactics being buggy, because the kernel
+will have to check their output.
+
+This chapter is divided in several sub-chapters:
+
+.. toctree::
+   :maxdepth: 1
+
+   ../gallina-specification-language
+   ../cic
+   ../../addendum/universe-polymorphism
+   ../../addendum/sprop
+   ../module-system
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
new file mode 100644
index 0000000000..5b5c2ab737
--- /dev/null
+++ b/doc/sphinx/language/extensions/index.rst
@@ -0,0 +1,28 @@
+.. _extensions:
+
+===================
+Language extensions
+===================
+
+Elaboration extends the language accepted by the Coq kernel to make it
+easier to use.  For example, this lets the user omit most type
+annotations because they can be inferred, call functions with implicit
+arguments which will be inferred as well, extend the syntax with
+notations, factorize branches when pattern-matching, etc.  In this
+chapter, we present these language extensions and we give some
+explanations on how this language is translated down to the core
+language presented in the :ref:`previous chapter <core-language>`.
+
+This chapter is divided in several sub-chapters:
+
+.. toctree::
+   :maxdepth: 1
+
+   ../gallina-extensions
+   ../../addendum/extended-pattern-matching
+   ../../user-extensions/syntax-extensions
+   ../../addendum/implicit-coercions
+   ../../addendum/type-classes
+   ../../addendum/canonical-structures
+   ../../addendum/program
+   ../../proof-engine/vernacular-commands
diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst
index 55c6d988f0..35837f8407 100644
--- a/doc/sphinx/license.rst
+++ b/doc/sphinx/license.rst
@@ -1,7 +1,7 @@
-License
--------
+.. note:: **License**
 
-This material (the Coq Reference Manual) may be distributed only subject to the
-terms and conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-http://www.opencontent.org/openpub). Options A and B are not elected.
+   This material (the Coq Reference Manual) may be distributed only
+   subject to the terms and conditions set forth in the Open
+   Publication License, v1.0 or later (the latest version is presently
+   available at http://www.opencontent.org/openpub). Options A and B
+   are not elected.
diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst
new file mode 100644
index 0000000000..e89bde63bc
--- /dev/null
+++ b/doc/sphinx/proofs/automatic-tactics/index.rst
@@ -0,0 +1,22 @@
+.. _automatic-tactics:
+
+=====================================================
+Built-in decision procedures and programmable tactics
+=====================================================
+
+Some tactics are largely automated and are able to solve complex
+goals.  This chapter presents both some decision procedures that can
+be used to solve some specific categories of goals, and some
+programmable tactics, that the user can instrument to handle some
+complex goals in new domains.
+
+This chapter is divided in several sub-chapters:
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../addendum/omega
+   ../../addendum/micromega
+   ../../addendum/ring
+   ../../addendum/nsatz
+   ../../addendum/generalized-rewriting
diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst
new file mode 100644
index 0000000000..5882f10ec3
--- /dev/null
+++ b/doc/sphinx/proofs/creating-tactics/index.rst
@@ -0,0 +1,35 @@
+.. _writing-tactics:
+
+====================
+Creating new tactics
+====================
+
+The languages presented in this chapter allow one to build complex
+tactics by combining existing ones with constructs such as
+conditionals and looping.  While :ref:`Ltac <ltac>` was initially
+thought of as a language for doing some basic combinations, it has
+been used successfully to build highly complex tactics as well, but
+this has also highlighted its limits and fragility.  The experimental
+language :ref:`Ltac2 <ltac2>` is a typed and more principled variant
+which is more adapted to building complex tactics.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../proof-engine/ltac
+   ../../proof-engine/ltac2
+
+
+There are other solutions beyond these two tactic languages to write
+new tactics:
+
+- `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin
+  which provides another typed tactic language.  While Ltac2 belongs
+  to the ML language family, Mtac2 reuses the language of Coq itself
+  as the language to build Coq tactics.
+
+- The most traditional way of building new complex tactics is to write
+  a Coq plugin in OCaml.  Beware that this also requires much more
+  effort and commitment.  A tutorial for writing Coq plugins is
+  available in the Coq repository in `doc/plugin_tutorial
+  <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
new file mode 100644
index 0000000000..cc4f7e1305
--- /dev/null
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -0,0 +1,34 @@
+.. _writing-proofs:
+
+==============
+Writing proofs
+==============
+
+Coq is an interactive theorem prover, or proof assistant, which means
+that proofs can be constructed interactively through a dialog between
+the user and the assistant.  The building blocks for this dialog are
+tactics which the user will use to represent steps in the proof of a
+theorem.
+
+Incomplete proofs have one or more open (unproven) sub-goals.  Each
+goal has its own context (a set of assumptions that can be used to
+prove the goal).  Tactics can transform goals and contexts.
+Internally, the incomplete proof is represented as a partial proof
+term, with holes for the unproven sub-goals.
+
+When a proof is complete, the user leaves the proof mode and defers
+the verification of the resulting proof term to the :ref:`kernel
+<core-language>`.
+
+This chapter is divided in several sub-chapters, describing the basic
+ideas of the proof mode (during which tactics can be used), and
+several flavors of tactics, including the SSReflect proof language:
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../proof-engine/proof-handling
+   ../../proof-engine/tactics
+   ../../proof-engine/ssreflect-proof-language
+   ../../proof-engine/detailed-tactic-examples
+   ../../user-extensions/proof-schemes
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