Merge PR #11601: [refman] Move chapters into new structure.

Reviewed-by: jfehrle

3 files changed, 88 insertions, 0 deletions

diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst
new file mode 100644
index 0000000000..a219770c69
--- /dev/null
+++ b/doc/sphinx/proofs/automatic-tactics/index.rst
@@ -0,0 +1,20 @@
+.. _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.
+
+.. 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..1af1b0b726
--- /dev/null
+++ b/doc/sphinx/proofs/creating-tactics/index.rst
@@ -0,0 +1,34 @@
+.. _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.
+
+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>`_.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../proof-engine/ltac
+   ../../proof-engine/ltac2
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
new file mode 100644
index 0000000000..a279a5957f
--- /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 parts, 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