Merge PR #13651: Shorten/improve intro of "Basic proof writing" chapter.

Reviewed-by: jfehrle

1 files changed, 9 insertions, 12 deletions

diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index 7724d7433c..63ddbd0a3a 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -10,19 +10,16 @@ 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.
+The first section presents the proof mode (the core mechanism of the
+dialog between the user and the proof assistant).  Then, several
+sections describe the available tactics.  One section covers the
+SSReflect proof language, which provides a consistent alternative set
+of tactics to the standard basic tactics.  The last section documents
+the ``Scheme`` family of commands, which can be used to extend the
+power of the :tacn:`induction` and :tacn:`inversion` tactics.
 
-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.
+Additional tactics are documented in the next chapter
+:ref:`automatic-tactics`.
 
 .. toctree::
    :maxdepth: 1