[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, 67 insertions, 0 deletions

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