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

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>`_.