Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaning

Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes

3 files changed, 76 insertions, 43 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index d77690458d..3ec6c118af 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -295,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write:
         end).
 
 But the possibility to use all the arguments is given by “``@``” implicit
-explicitations (as for terms 2.7.11).
+explicitations (as for terms, see :ref:`explicit-applications`).
 
 .. coqtop:: all
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ec97377128..0bcca0fe56 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2762,14 +2762,14 @@ typeclass inference.
 
      Goal True.
 
-+ .. coqtop:: in undo
+  .. coqdoc::
 
      have foo : ty.
 
   Full inference for ``ty``. The first subgoal demands a
   proof of such instantiated statement.
 
-+ .. coqdoc::
+  .. coqdoc::
 
      have foo : ty := .
 
@@ -2778,13 +2778,13 @@ typeclass inference.
   statement. Note that no proof term follows ``:=``, hence two subgoals are
   generated.
 
-+ .. coqtop:: in undo
+  .. coqdoc::
 
      have foo : ty := t.
 
   No inference for ``ty`` and ``t``.
 
-+ .. coqtop:: in undo
+  .. coqdoc::
 
      have foo := t.
 
@@ -4586,13 +4586,18 @@ disjunction.
 
      Lemma test a : P (a || a) -> True.
 
-  .. coqtop:: all undo
+  .. coqtop:: all
 
      move=> HPa; move/P2Q: HPa => HQa.
 
   or more directly:
 
-  .. coqtop:: all undo
+  .. coqtop:: none
+
+     Abort.
+     Lemma test a : P (a || a) -> True.
+
+  .. coqtop:: all
 
      move/P2Q=> HQa.
 
@@ -4890,11 +4895,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``.
 
      Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2).
 
-  .. coqtop:: all undo
+  .. coqtop:: all
 
      case: (@andE b1 b2).
 
-  .. coqtop:: all undo
+  .. coqtop:: none
+
+     Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2).
+
+  .. coqtop:: all
 
      case: (@andP b1 b2).
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 0bcfce2322..d58cbdec07 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -755,33 +755,49 @@ Applying theorems
 
    A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``.
 
-   .. coqtop:: all undo
+   .. coqtop:: all
 
       apply (Rtrans n m p).
 
    Note that ``n`` can be inferred from the goal, so the following would work
    too.
 
-   .. coqtop:: in undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: in
 
       apply (Rtrans _ m).
 
    More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the
    unknown m:
 
-   .. coqtop:: in undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: in
 
       apply Rtrans with (y := m).
 
    Another solution is to mention the proof of ``(R x y)`` in ``Rtrans``
 
-   .. coqtop:: all undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: all
 
       apply Rtrans with (1 := Rnm).
 
    ... or the proof of ``(R y z)``.
 
-   .. coqtop:: all undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: all
 
       apply Rtrans with (2 := Rmp).
 
@@ -789,6 +805,10 @@ Applying theorems
    finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This
    instantiates the existential variable and completes the proof.
 
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
    .. coqtop:: all
 
       eapply Rtrans.
@@ -2332,6 +2352,7 @@ and an explanation of the underlying technique.
    where :n:`@ident` is the identifier for the last introduced hypothesis.
 
 .. tacv:: inversion_clear @ident
+   :name: inversion_clear
 
    This behaves as :n:`inversion` and then erases :n:`@ident` from the context.
 
@@ -2490,47 +2511,54 @@ and an explanation of the underlying technique.
 
    *Non-dependent inversion*.
 
-   Let us consider the relation Le over natural numbers and the following
-   variables:
+   Let us consider the relation :g:`Le` over natural numbers:
 
-   .. coqtop:: all reset
+   .. coqtop:: reset in
 
       Inductive Le : nat -> nat -> Set :=
       | LeO : forall n:nat, Le 0 n
       | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-      Variable P : nat -> nat -> Prop.
-      Variable Q : forall n m:nat, Le n m -> Prop.
+
 
    Let us consider the following goal:
 
    .. coqtop:: none
 
+      Section Section.
+      Variable P : nat -> nat -> Prop.
+      Variable Q : forall n m:nat, Le n m -> Prop.
       Goal forall n m, Le (S n) m -> P n m.
       intros.
 
-   .. coqtop:: all
+   .. coqtop:: out
 
       Show.
 
-   To prove the goal, we may need to reason by cases on H and to derive
-   that m is necessarily of the form (S m 0 ) for certain m 0 and that
-   (Le n m 0 ). Deriving these conditions corresponds to proving that the
-   only possible constructor of (Le (S n) m) isLeS and that we can invert
-   the-> in the type of LeS. This inversion is possible because Le is the
-   smallest set closed by the constructors LeO and LeS.
+   To prove the goal, we may need to reason by cases on :g:`H` and to derive
+   that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that
+   :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only
+   possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert
+   the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le`
+   is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`.
 
-   .. coqtop:: undo all
+   .. coqtop:: all
 
       inversion_clear H.
 
-   Note that m has been substituted in the goal for (S m0) and that the
-   hypothesis (Le n m0) has been added to the context.
+   Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the
+   hypothesis :g:`(Le n m0)` has been added to the context.
 
-   Sometimes it is interesting to have the equality m=(S m0) in the
-   context to use it after. In that case we can use inversion that does
+   Sometimes it is interesting to have the equality :g:`m = (S m0)` in the
+   context to use it after. In that case we can use :tacn:`inversion` that does
    not clear the equalities:
 
-   .. coqtop:: undo all
+   .. coqtop:: none
+
+      Abort.
+      Goal forall n m, Le (S n) m -> P n m.
+      intros.
+
+   .. coqtop:: all
 
       inversion H.
 
@@ -2540,31 +2568,27 @@ and an explanation of the underlying technique.
 
    Let us consider the following goal:
 
-   .. coqtop:: reset none
+   .. coqtop:: none
 
-      Inductive Le : nat -> nat -> Set :=
-      | LeO : forall n:nat, Le 0 n
-      | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-      Variable P : nat -> nat -> Prop.
-      Variable Q : forall n m:nat, Le n m -> Prop.
+      Abort.
       Goal forall n m (H:Le (S n) m), Q (S n) m H.
       intros.
 
-   .. coqtop:: all
+   .. coqtop:: out
 
       Show.
 
-   As H occurs in the goal, we may want to reason by cases on its
-   structure and so, we would like inversion tactics to substitute H by
+   As :g:`H` occurs in the goal, we may want to reason by cases on its
+   structure and so, we would like inversion tactics to substitute :g:`H` by
    the corresponding @term in constructor form. Neither :tacn:`inversion` nor
-   :n:`inversion_clear` do such a substitution. To have such a behavior we
+   :tacn:`inversion_clear` do such a substitution. To have such a behavior we
    use the dependent inversion tactics:
 
    .. coqtop:: all
 
       dependent inversion_clear H.
 
-   Note that H has been substituted by (LeS n m0 l) andm by (S m0).
+   Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`.
 
 .. example::