Using options abort and restart of coqtop directive in the manual.

8 files changed, 64 insertions, 225 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index cc788b3595..b474c51f17 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -627,14 +627,10 @@ logical equivalence:
    Instance all_iff_morphism (A : Type) :
             Proper (pointwise_relation A iff ==> iff) (@all A).
 
-.. coqtop:: all
+.. coqtop:: all abort
 
    Proof. simpl_relation.
 
-.. coqtop:: none
-
-   Abort.
-
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
 declared such a morphism, it will be used by the setoid rewriting
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 963242ea72..c1eab8a970 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -264,17 +264,13 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``,
 ``f_equal4`` and ``f_equal5``.
 For instance ``f_equal3`` is defined the following way.
 
-.. coqtop:: in
+.. coqtop:: in abort
   
   Theorem f_equal3 :
    forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
      (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
      x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
 
-.. coqtop:: none
-
-   Abort.
-
 .. _datatypes:
 
 Datatypes
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 933f07674a..2f99368f48 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1967,14 +1967,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
       and :g:`B` can be synthesized in the next statement.
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Lemma is_law_S : is_law S.
 
-      .. coqtop:: none
-
-         Abort.
-
    .. note::
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index bd16b70d02..63d6a229ed 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -53,7 +53,7 @@ rule of thumb, all the variables that appear inside constructors in
 the indices of the hypothesis should be generalized. This is exactly
 what the ``generalize_eqs_vars`` variant does:
 
-.. coqtop:: all
+.. coqtop:: all abort
 
    generalize_eqs_vars H.
    induction H.
@@ -65,7 +65,7 @@ as well in this case, e.g.:
 
 .. coqtop:: none
 
-   Abort.
+   Require Import Coq.Program.Equality.
 
 .. coqtop:: in
 
@@ -88,11 +88,7 @@ automatically do such simplifications (which may involve the axiom K).
 This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality``
 does. For example, we might simplify the previous goals considerably:
 
-.. coqtop:: all
-
-   Require Import Coq.Program.Equality.
-
-.. coqtop:: all
+.. coqtop:: all abort
 
    induction p ; simplify_dep_elim.
 
@@ -105,10 +101,6 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or
 simply case analysis on the generalized hypothesis. For example we can
 redo what we’ve done manually with dependent destruction:
 
-.. coqtop:: none
-
-   Abort.
-
 .. coqtop:: in
 
    Lemma ex : forall n m:nat, Le (S n) m -> P n m.
@@ -117,7 +109,7 @@ redo what we’ve done manually with dependent destruction:
 
    intros n m H.
 
-.. coqtop:: all
+.. coqtop:: all abort
 
    dependent destruction H.
 
@@ -126,10 +118,6 @@ destructed hypothesis actually appeared in the goal, the tactic would
 still be able to invert it, contrary to dependent inversion. Consider
 the following example on vectors:
 
-.. coqtop:: none
-
-   Abort.
-
 .. coqtop:: in
 
    Set Implicit Arguments.
@@ -230,29 +218,21 @@ name. A term is either an application of:
 
 Once we have this datatype we want to do proofs on it, like weakening:
 
-.. coqtop:: in
+.. coqtop:: in abort
 
    Lemma weakening : forall G D tau, term (G ; D) tau -> 
                      forall tau', term (G , tau' ; D) tau.
 
-.. coqtop:: none
-
-   Abort.
-
 The problem here is that we can’t just use induction on the typing
 derivation because it will forget about the ``G ; D`` constraint appearing
 in the instance. A solution would be to rewrite the goal as:
 
-.. coqtop:: in
+.. coqtop:: in abort
 
    Lemma weakening' : forall G' tau, term G' tau ->
                       forall G D, (G ; D) = G' ->
                       forall tau', term (G, tau' ; D) tau.
 
-.. coqtop:: none
-
-   Abort.
-
 With this proper separation of the index from the instance and the
 right induction loading (putting ``G`` and ``D`` after the inducted-on
 hypothesis), the proof will go through, but it is a very tedious
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c1da1112c8..3e87e8acd8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -701,7 +701,7 @@ tactic
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Ltac time_constr1 tac :=
            let eval_early := match goal with _ => restart_timer "(depth 1)" end in
@@ -716,7 +716,6 @@ tactic
                         let y := time_constr1 ltac:(fun _ => eval compute in x) in
                         y) in
            pose v.
-         Abort.
 
 Local definitions
 ~~~~~~~~~~~~~~~~~
@@ -847,7 +846,7 @@ We can carry out pattern matching on terms with:
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Ltac f x :=
            match x with
@@ -859,10 +858,6 @@ We can carry out pattern matching on terms with:
          Goal True.
          f (3+4).
 
-      .. coqtop:: none
-
-         Abort.
-
 .. _ltac-match-goal:
 
 Pattern matching on goals
@@ -1026,14 +1021,10 @@ Counting the goals
          Goal True /\ True /\ True.
          split;[|split].
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          all:pr_numgoals.
 
-      .. coqtop:: none
-
-         Abort.
-
 Testing boolean expressions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1318,10 +1309,10 @@ performance issue.
 
 .. coqtop:: all
 
-  Set Ltac Profiling.
-  tac.
-  Show Ltac Profile.
-  Show Ltac Profile "omega".
+   Set Ltac Profiling.
+   tac.
+   Show Ltac Profile.
+   Show Ltac Profile "omega".
 
 .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 24645a8cc3..2300a317f1 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -529,16 +529,12 @@ Requesting information
 
       .. example::
 
-         .. coqtop:: all
+         .. coqtop:: all abort
 
             Goal exists n, n = 0.
             eexists ?[n].
             Show n.
 
-         .. coqtop:: none
-
-            Abort.
-
    .. cmdv:: Show Script
       :name: Show Script
 
@@ -739,14 +735,10 @@ Notes:
 
       split.
 
-    .. coqtop:: all
+    .. coqtop:: all abort
 
       2: split.
 
-    .. coqtop:: none
-
-      Abort.
-
   ..
 
     .. coqtop:: none
@@ -759,14 +751,10 @@ Notes:
 
        intros n.
 
-    .. coqtop:: all
+    .. coqtop:: all abort
 
       intros m.
 
-    .. coqtop:: none
-
-      Abort.
-
 This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal
 with 2 goals.  Notice that the goal ``P 1`` is not highlighted at all after
 the split because it has not changed.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4675fe3248..3580f6824f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -652,11 +652,7 @@ The tactic:
       Lemma test x :  f x + f x = f x.
       set t := f _.
 
-   .. coqtop:: none
-
-      Undo.
-
-   .. coqtop:: all
+   .. coqtop:: all restart
 
       set t := {2}(f _).
 
@@ -1989,19 +1985,17 @@ be substituted.
          Lemma test l : (length l) * 2 = length (l ++ l).
          case: (lastP l).
 
-      Applied to the same goal, the command:
-      ``case: l / (lastP l).``
-      generates the same subgoals but ``l`` has been cleared from both contexts.
+      Applied to the same goal, the tactc ``case: l / (lastP l)``
+      generates the same subgoals but ``l`` has been cleared from both contexts:
 
-      Again applied to the same goal, the command.
+      .. coqtop:: all restart
 
-      .. coqtop:: none
+         case: l / (lastP l).
 
-         Abort.
+      Again applied to the same goal:
 
-      .. coqtop:: all
+      .. coqtop:: all restart abort
 
-         Lemma test l : (length l) * 2 = length (l ++ l).
          case: {1 3}l / (lastP l).
 
       Note that selected occurrences on the left of the ``/``
@@ -2015,10 +2009,6 @@ be substituted.
 
    .. example::
 
-      .. coqtop:: none
-
-         Abort.
-
       .. coqtop:: all
 
          Lemma test l : (length l) * 2 = length (l ++ l).
@@ -2634,7 +2624,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity,
 bound variables can be surrounded
 with parentheses even if no type is specified:
 
-.. coqdoc::
+.. coqtop:: all restart
 
    have (x) : 2 * x = x + x by omega.
 
@@ -2648,13 +2638,8 @@ copying the goal itself.
 
 .. example::
 
-  .. coqtop:: none
+  .. coqtop:: all restart abort
 
-     Abort All.
-
-  .. coqtop:: all
-
-     Lemma test : True.
      have suff H : 2 + 2 = 3; last first.
 
   Note that H is introduced in the second goal.
@@ -2675,10 +2660,9 @@ context entry name.
 
   .. coqtop:: none
 
-     Abort All.
      Set Printing Depth 15.
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Inductive Ord n := Sub x of x < n.
      Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n").
@@ -2694,11 +2678,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort All.
-
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
      have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega.
@@ -2711,11 +2691,7 @@ with have and an explicit term, they must be used as follows:
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort All.
-
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
      have [:pm] @i : 'I_n := Sub m pm.
@@ -2734,11 +2710,7 @@ makes use of it).
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort All.
-
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
      have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega.
@@ -2755,20 +2727,20 @@ typeclass inference.
 
   .. coqtop:: none
 
-     Abort All.
-
      Axiom ty : Type.
      Axiom t : ty.
 
      Goal True.
 
-  .. coqdoc::
+  .. coqtop:: all
 
      have foo : ty.
 
   Full inference for ``ty``. The first subgoal demands a
   proof of such instantiated statement.
 
+  .. A strange bug prevents using the coqtop directive here
+
   .. coqdoc::
 
      have foo : ty := .
@@ -2778,13 +2750,13 @@ typeclass inference.
   statement. Note that no proof term follows ``:=``, hence two subgoals are
   generated.
 
-  .. coqdoc::
+  .. coqtop:: all restart
 
      have foo : ty := t.
 
   No inference for ``ty`` and ``t``.
 
-  .. coqdoc::
+  .. coqtop:: all restart abort
 
      have foo := t.
 
@@ -2833,10 +2805,9 @@ The ``have`` modifier can follow the ``suff`` tactic.
 
   .. coqtop:: none
 
-     Abort All.
      Axioms G P : Prop.
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test : G.
      suff have H : P.
@@ -2901,10 +2872,6 @@ are unique.
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort All.
-
   .. coqtop:: all
 
      Lemma quo_rem_unicity d q1 q2 r1 r2 :
@@ -3135,7 +3102,7 @@ An :token:`r_item` can be:
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
 
-     .. coqtop:: all
+     .. coqtop:: all abort
 
         Definition double x := x + x.
         Definition ddouble x := double (double x).
@@ -3147,21 +3114,16 @@ An :token:`r_item` can be:
      The |SSR| terms containing holes are *not* typed as
      abstractions in this context. Hence the following script fails.
 
-     .. coqtop:: none
-
-        Abort.
-
      .. coqtop:: all
 
         Definition f := fun x y => x + y.
         Lemma test x y : x + y = f y x.
-        Fail rewrite -[f y]/(y + _).
 
-     but the following script succeeds
+     .. coqtop:: fail
 
-     .. coqtop:: none
+        rewrite -[f y]/(y + _).
 
-        Restart.
+     but the following script succeeds
 
      .. coqtop:: all
 
@@ -3399,7 +3361,7 @@ rewrite operations prescribed by the rules on the current goal.
 
      Section Test.
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Variables (a b c : nat).
      Hypothesis eqab : a = b.
@@ -3413,10 +3375,6 @@ rewrite operations prescribed by the rules on the current goal.
   ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a
   definition:
 
-  .. coqtop:: none
-
-     Abort.
-
   .. coqtop:: all
 
      Definition multi1 := (eqab, eqac).
@@ -3433,7 +3391,7 @@ literal matches have priority.
 
 .. example::
 
-   .. coqtop:: all
+   .. coqtop:: all abort
 
       Definition d := a.
       Hypotheses eqd0 : d = 0.
@@ -3450,11 +3408,7 @@ repeated anew.
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort.
-
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Hypothesis eq_adda_b : forall x, x + a = b.
      Hypothesis eq_adda_c : forall x, x + a = c.
@@ -3477,10 +3431,6 @@ tactic rewrite ``(=~ multi1)`` is equivalent to ``rewrite multi1_rev``.
 
 .. example::
 
-  .. coqtop:: none
-
-     Abort.
-
   .. coqtop:: all
 
      Hypothesis eqba : b = a.
@@ -3552,11 +3502,7 @@ Anyway this tactic is *not* equivalent to
 
   while the other tactic results in
 
-  .. coqtop:: none
-
-     Undo.
-
-  .. coqtop:: all
+  .. coqtop:: restart abort
 
      rewrite (_ : forall x, x * 0 = 0).
 
@@ -3613,13 +3559,9 @@ cases:
     there is no occurrence of the head symbol ``f`` of the rewrite rule in the
     goal.
 
-    .. coqtop:: none
-
-       Undo.
-
-    .. coqtop:: all
+    .. coqtop:: all restart fail
 
-       Fail rewrite H.
+       rewrite H.
 
     Rewriting with ``H`` first requires unfolding the occurrences of
     ``f``
@@ -3627,21 +3569,13 @@ cases:
     occurrence), using tactic ``rewrite /f`` (for a global replacement of
     f by g) or ``rewrite pattern/f``, for a finer selection.
 
-    .. coqtop:: none
-
-       Undo.
-
-    .. coqtop:: all
+    .. coqtop:: all restart
 
        rewrite /f H.
 
     alternatively one can override the pattern inferred from ``H``
 
-    .. coqtop:: none
-
-       Undo.
-
-    .. coqtop:: all
+    .. coqtop:: all restart
 
        rewrite [f _]H.
 
@@ -3668,7 +3602,7 @@ corresponding new goals will be generated.
      Unset Printing Implicit Defensive.
      Set Warnings "-notation-overridden".
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Axiom leq : nat -> nat -> bool.
      Notation "m <= n" := (leq m n) : nat_scope.
@@ -3691,10 +3625,6 @@ corresponding new goals will be generated.
   As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to
   solve the existential variable.
 
-  .. coqtop:: none
-
-     Abort.
-
   .. coqtop:: all
 
      Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y.
@@ -4592,12 +4522,7 @@ disjunction.
 
   or more directly:
 
-  .. coqtop:: none
-
-     Abort.
-     Lemma test a : P (a || a) -> True.
-
-  .. coqtop:: all
+  .. coqtop:: all restart
 
      move/P2Q=> HQa.
 
@@ -4931,17 +4856,13 @@ The view mechanism is compatible with reflect predicates.
      Unset Printing Implicit Defensive.
      Section Test.
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b.
      apply/andP.
 
   Conversely
 
-  .. coqtop:: none
-
-     Abort.
-
   .. coqtop:: all
 
      Lemma test (a b : bool) : a /\ b -> a.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6f57cc53a9..0b13c6486b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -749,9 +749,9 @@ Applying theorems
    The direct application of ``Rtrans`` with ``apply`` fails because no value
    for ``y`` in ``Rtrans`` is found by ``apply``:
 
-   .. coqtop:: all
+   .. coqtop:: all fail
 
-      Fail apply Rtrans.
+      apply Rtrans.
 
    A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``.
 
@@ -762,42 +762,26 @@ Applying theorems
    Note that ``n`` can be inferred from the goal, so the following would work
    too.
 
-   .. coqtop:: none
-
-      Abort. Goal R n p.
-
-   .. coqtop:: in
+   .. coqtop:: in restart
 
       apply (Rtrans _ m).
 
    More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the
    unknown m:
 
-   .. coqtop:: none
-
-      Abort. Goal R n p.
-
-   .. coqtop:: in
+   .. coqtop:: in restart
 
       apply Rtrans with (y := m).
 
    Another solution is to mention the proof of ``(R x y)`` in ``Rtrans``
 
-   .. coqtop:: none
-
-      Abort. Goal R n p.
-
-   .. coqtop:: all
+   .. coqtop:: all restart
 
       apply Rtrans with (1 := Rnm).
 
    ... or the proof of ``(R y z)``.
 
-   .. coqtop:: none
-
-      Abort. Goal R n p.
-
-   .. coqtop:: all
+   .. coqtop:: all restart
 
       apply Rtrans with (2 := Rmp).
 
@@ -805,11 +789,7 @@ 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
+   .. coqtop:: all restart abort
 
       eapply Rtrans.
 
@@ -2528,11 +2508,10 @@ and an explanation of the underlying technique.
       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:: out
 
-      Show.
+      intros.
 
    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
@@ -2552,10 +2531,7 @@ and an explanation of the underlying technique.
    context to use it after. In that case we can use :tacn:`inversion` that does
    not clear the equalities:
 
-   .. coqtop:: none
-
-      Abort.
-      Goal forall n m, Le (S n) m -> P n m.
+   .. coqtop:: none restart
       intros.
 
    .. coqtop:: all
@@ -2572,11 +2548,10 @@ and an explanation of the underlying technique.
 
       Abort.
       Goal forall n m (H:Le (S n) m), Q (S n) m H.
-      intros.
 
    .. coqtop:: out
 
-      Show.
+      intros.
 
    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
@@ -3345,7 +3320,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Goal ~0=0.
          unfold not.
@@ -3353,10 +3328,6 @@ the conversion in hypotheses :n:`{+ @ident}`.
          pattern (0 = 0).
          fold not.
 
-      .. coqtop:: none
-
-         Abort.
-
    .. tacv:: fold {+ @term}
 
       Equivalent to :n:`fold @term ; ... ; fold @term`.