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

1 files changed, 34 insertions, 0 deletions

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