Merge PR #9501: Sphinx: fail when a command fails + other stuff

Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego

15 files changed, 283 insertions, 387 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 5861b18d2b..fac0035de1 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -214,17 +214,17 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
 
     Example::
 
-       .. coqtop:: in undo
+       .. coqtop:: in reset
 
           Print nat.
           Definition a := 1.
 
     The blank line after the directive is required.  If you begin a proof,
-    include an ``Abort`` afterwards to reset coqtop for the next example.
+    use the ``abort`` option to reset coqtop for the next example.
 
     Here is a list of permissible options:
 
-    - Display options
+    - Display options (choose exactly one)
 
       - ``all``: Display input and output
       - ``in``: Display only input
@@ -234,7 +234,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``undo``: Reset state after executing. Not compatible with ``reset``.
+      - ``fail``: Don't die if a command fails
+      - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
+      - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
@@ -508,7 +510,7 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
    .. coqtop:: all
 
@@ -518,7 +520,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents.
 
       Lemma l2: 2 + 2 <> 1.
 
-Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
 
 Abbreviations and macros
 ------------------------
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 81f25bf274..78803a927f 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -265,7 +265,7 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
    .. coqtop:: all
 
@@ -275,7 +275,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents.
 
       Lemma l2: 2 + 2 <> 1.
 
-Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
 
 Abbreviations and macros
 ------------------------
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/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 43d302114e..c7ea7e326f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is:
       eqb_leibniz x y H :=
             match x, y return x = y with tt, tt => eq_refl tt end }.
 
-If one does not give all the members in the Instance declaration, Coq
-enters the proof-mode and the user is asked to build inhabitants of
-the remaining fields, e.g.:
+Using :cmd:`Program Instance`, if one does not give all the members in
+the Instance declaration, Coq generates obligations for the remaining
+fields, e.g.:
 
 .. coqtop:: in
 
-   Instance eq_bool : EqDec bool :=
+   Require Import Program.Tactics.
+   Program Instance eq_bool : EqDec bool :=
    { eqb x y := if x then y else negb y }.
 
 .. coqtop:: all
 
-   Proof. intros x y H.
-
-.. coqtop:: all
-
-   destruct x ; destruct y ; (discriminate || reflexivity).
-
-.. coqtop:: all
-
+   Next Obligation.
+     destruct x ; destruct y ; (discriminate || reflexivity).
    Defined.
 
 One has to take care that the transparency of every field is
@@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.:
 
 .. coqtop:: in
 
-   Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
+   Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
    { eqb x y := match x, y with
                 | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
                 end }.
 
 .. coqtop:: none
 
-   Abort.
+   Admit Obligations.
 
 These instances are used just as well as lemmas in the instance hint
 database.
@@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example:
 
      Context `{EA : EqDec A}.
 
-     Global Instance option_eqb : EqDec (option A) :=
+     Global Program Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
             | None, None => true
             | _, _ => false
             end }.
-     Admitted.
+   Admit Obligations.
 
    End EqDec_defs.
 
@@ -564,12 +559,12 @@ Settings
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
-   + When it is on (the default), instances that have unsolved holes in
+   + When it is off (the default), they fail with an error instead.
+
+   + When it is on, instances that have unsolved holes in
      their proof-term silently open the proof mode with the remaining
      obligations to prove.
 
-   + When it is off, they fail with an error instead.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
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 d2fd08536a..25f983ac1e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1962,14 +1962,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/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 1b4d2315aa..eebf1f11e1 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel
 with the command ``Drop.``, and come back to the |Coq|
 toplevel with the command ``Coqloop.loop();;``.
 
+.. flag:: Coqtop Exit On Error
+
+   This option, off by default, causes coqtop to exit with status code
+   ``1`` if a command produces an error instead of recovering from it.
+
 Batch compilation (coqc)
 ------------------------
 
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 c134563efe..3e87e8acd8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -602,7 +602,7 @@ Failing
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all fail
 
          Goal True.
          Proof. fail. Abort.
@@ -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 0bcca0fe56..237b534d67 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -215,7 +215,7 @@ construct differs from the latter in that
 
   .. example::
 
-    .. coqtop:: reset
+    .. coqtop:: reset none
 
        From Coq Require Import ssreflect.
        Set Implicit Arguments.
@@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows:
 
 .. example::
 
-    .. coqtop:: reset
+    .. coqtop:: reset none
 
        From Coq Require Import ssreflect.
        Set Implicit Arguments.
@@ -376,7 +376,7 @@ expressions such as
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -401,7 +401,7 @@ each point of use, e.g., the above definition can be written:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -464,7 +464,7 @@ defined by the following declaration:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -518,7 +518,7 @@ For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters:
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -639,7 +639,7 @@ The tactic:
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -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 _).
 
@@ -694,7 +690,7 @@ conditions:
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -715,7 +711,7 @@ conditions:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -736,7 +732,7 @@ Moreover:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -756,7 +752,7 @@ Moreover:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -789,7 +785,7 @@ An *occurrence switch* can be:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -810,7 +806,7 @@ An *occurrence switch* can be:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -831,7 +827,7 @@ An *occurrence switch* can be:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -862,7 +858,7 @@ selection.
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -879,7 +875,7 @@ only one occurrence of the selected term.
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -910,7 +906,7 @@ context of a goal thanks to the ``in`` tactical.
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
 
@@ -926,7 +922,7 @@ context of a goal thanks to the ``in`` tactical.
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
 
@@ -1042,7 +1038,7 @@ constants to the goal.
 
    For example, the proof of [#3]_
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -1104,7 +1100,7 @@ The ``:`` tactical is used to operate on an element in the context.
    to encapsulate the inductive step in a single
    command:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -1257,7 +1253,7 @@ The elim tactic
 
    .. example::
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -1297,7 +1293,7 @@ existential metavariables of sort :g:`Prop`.
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -1477,7 +1473,7 @@ context to interpret wildcards; in particular it can accommodate the
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -1752,7 +1748,7 @@ Clears are deferred until the end of the intro pattern.
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect ssrbool.
       Set Implicit Arguments.
@@ -1813,7 +1809,7 @@ Block introduction
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
@@ -1866,7 +1862,7 @@ deal with the possible parameters of the constants introduced.
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -1885,7 +1881,7 @@ under fresh |SSR| names.
 
 .. example::
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -1952,7 +1948,7 @@ be substituted.
       Here is a small example on lists. We define first a function which
       adds an element at the end of a given list.
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -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).
@@ -2260,7 +2250,7 @@ to the others.
    Here is a small example on lists. We define first a function which
    adds an element at the end of a given list.
 
-   .. coqtop:: reset
+   .. coqtop:: reset none
 
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
@@ -2379,7 +2369,7 @@ between standard Ltac in and the |SSR| tactical in.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2454,7 +2444,7 @@ the holes are abstracted in term.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2468,7 +2458,7 @@ the holes are abstracted in term.
 
   The invokation of ``have`` is equivalent to:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2486,7 +2476,7 @@ tactic:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2539,7 +2529,7 @@ the further use of the intermediate step. For instance,
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2567,7 +2557,7 @@ destruction of existential assumptions like in the tactic:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2594,7 +2584,7 @@ term for the intermediate lemma, using tactics of the form:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2615,7 +2605,7 @@ After the :token:`i_pattern`, a list of binders is allowed.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      From Coq Require Import Omega.
@@ -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 :
@@ -2926,7 +2893,7 @@ pattern will be used to process its instance.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrfun ssrbool.
      Set Implicit Arguments.
@@ -2975,7 +2942,7 @@ illustrated in the following example.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -2994,7 +2961,7 @@ illustrated in the following example.
   the pattern ``id (addx x)``, that would produce the following first
   subgoal
 
-  .. coqtop:: none reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect Omega.
      Set Implicit Arguments.
@@ -3128,14 +3095,14 @@ An :token:`r_item` can be:
 
   .. example::
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect.
         Set Implicit Arguments.
         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:: all fail
 
-     .. coqtop:: none
+        rewrite -[f y]/(y + _).
 
-        Restart.
+     but the following script succeeds
 
      .. coqtop:: all
 
@@ -3252,7 +3214,7 @@ proof of basic results on natural numbers arithmetic.
 .. example::
 
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3288,7 +3250,7 @@ side of the equality the user wants to rewrite.
 .. example::
 
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3308,7 +3270,7 @@ the equality.
 .. example::
 
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3331,7 +3293,7 @@ Occurrence switches and redex switches
 .. example::
 
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3360,7 +3322,7 @@ repetition.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3390,7 +3352,7 @@ rewrite operations prescribed by the rules on the current goal.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -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.
@@ -3536,7 +3486,7 @@ Anyway this tactic is *not* equivalent to
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3552,11 +3502,7 @@ Anyway this tactic is *not* equivalent to
 
   while the other tactic results in
 
-  .. coqtop:: none
-
-     Undo.
-
-  .. coqtop:: all
+  .. coqtop:: all restart abort
 
      rewrite (_ : forall x, x * 0 = 0).
 
@@ -3590,7 +3536,7 @@ cases:
 
   .. example::
 
-    .. coqtop:: reset
+    .. coqtop:: reset none
 
        From Coq Require Import ssreflect.
        Set Implicit Arguments.
@@ -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.
 
@@ -3660,7 +3594,7 @@ corresponding new goals will be generated.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrfun ssrbool.
      Set Implicit Arguments.
@@ -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.
@@ -3743,7 +3673,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrfun ssrbool.
      From Coq Require Import List.
@@ -3767,7 +3697,7 @@ definition.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -3877,7 +3807,7 @@ which the function is supplied:
 
    .. example::
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -3904,7 +3834,7 @@ which the function is supplied:
 
    .. example::
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -3927,7 +3857,7 @@ which the function is supplied:
 
    .. example::
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -3948,7 +3878,7 @@ which the function is supplied:
 
    .. example::
 
-      .. coqtop:: reset
+      .. coqtop:: reset none
 
          From Coq Require Import ssreflect.
          Set Implicit Arguments.
@@ -4128,7 +4058,7 @@ parentheses are required around more complex patterns.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4167,7 +4097,7 @@ Contextual patterns in rewrite
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4331,7 +4261,7 @@ generation (see section :ref:`generation_of_equations_ssr`).
    The following script illustrates a toy example of this feature. Let us
    define a function adding an element at the end of a list:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect List.
      Set Implicit Arguments.
@@ -4406,7 +4336,7 @@ Here is an example of a regular, but nontrivial, eliminator.
 
   Here is a toy example illustrating this feature.
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect FunInd.
      Set Implicit Arguments.
@@ -4433,7 +4363,7 @@ Here is an example of a regular, but nontrivial, eliminator.
      elim/plus_ind: {z}_.
      elim/plus_ind: z / _.
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect FunInd.
      Set Implicit Arguments.
@@ -4458,7 +4388,7 @@ Here is an example of a regular, but nontrivial, eliminator.
   ``plus (plus x y) z`` thus instantiating the last ``_`` with ``z``.
   Note that the tactic:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect FunInd.
      Set Implicit Arguments.
@@ -4488,7 +4418,7 @@ Here is an example of a truncated eliminator:
 
   Consider the goal:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect FunInd.
      Set Implicit Arguments.
@@ -4552,7 +4482,7 @@ disjunction.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4573,7 +4503,7 @@ disjunction.
   This operation is so common that the tactic shell has specific
   syntax for it. The following scripts:
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -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.
 
@@ -4613,7 +4538,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4646,7 +4571,7 @@ relevant for the current goal.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4690,7 +4615,7 @@ assumption to some given arguments.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4719,7 +4644,7 @@ bookkeeping steps.
    The following example use the ``~~`` prenex notation for boolean negation:
 
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -4775,7 +4700,7 @@ analysis:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
      Set Implicit Arguments.
@@ -4792,7 +4717,7 @@ analysis
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -4847,7 +4772,7 @@ For instance, the following lemma:
 
 .. coqdoc::
 
-     Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2).
+   Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2).
 
 relates the boolean conjunction to the logical one ``/\``. Note that in
 ``andP``, ``b1`` and ``b2`` are two boolean variables and the
@@ -4882,7 +4807,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -4901,7 +4826,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``.
 
   .. coqtop:: none
 
-     Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2).
+     Restart.
 
   .. coqtop:: all
 
@@ -4923,7 +4848,7 @@ The view mechanism is compatible with reflect predicates.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -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.
@@ -5045,7 +4966,7 @@ but they also allow complex transformation, involving negations.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -5078,7 +4999,7 @@ actually uses its propositional interpretation.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -5140,7 +5061,7 @@ In this context, the identity view can be used when no view has to be applied:
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -5156,7 +5077,7 @@ In this context, the identity view can be used when no view has to be applied:
   The same goal can be decomposed in several ways, and the user may
   choose the most convenient interpretation.
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -5232,7 +5153,7 @@ pass a given hypothesis to a lemma.
 
 .. example::
 
-  .. coqtop:: reset
+  .. coqtop:: reset none
 
      From Coq Require Import ssreflect ssrbool.
      Set Implicit Arguments.
@@ -5291,7 +5212,7 @@ equivalences are indeed taken into account, otherwise only single
      looks for any notation that contains fragment as a substring. If the
      ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers :
 
-     .. coqtop:: reset
+     .. coqtop:: reset none
 
         From Coq Require Import ssreflect ssrbool.
         Set Implicit Arguments.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6f57cc53a9..b5e9a902c6 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,8 @@ 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
+   .. coqtop:: none restart
 
-      Abort.
-      Goal forall n m, Le (S n) m -> P n m.
       intros.
 
    .. coqtop:: all
@@ -2572,11 +2549,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 +3321,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Goal ~0=0.
          unfold not.
@@ -3353,10 +3329,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`.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0dd9b3aa3e..8df0f2be97 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -30,7 +30,7 @@ from sphinx import addnodes
 from sphinx.roles import XRefRole
 from sphinx.errors import ExtensionError
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
-from sphinx.util.logging import getLogger
+from sphinx.util.logging import getLogger, get_node_location
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
 from sphinx.domains.std import token_xrefs
@@ -38,7 +38,7 @@ from sphinx.ext import mathbase
 
 from . import coqdoc
 from .repl import ansicolors
-from .repl.coqtop import CoqTop
+from .repl.coqtop import CoqTop, CoqTopError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
@@ -560,17 +560,17 @@ class CoqtopDirective(Directive):
 
     Example::
 
-       .. coqtop:: in undo
+       .. coqtop:: in reset
 
           Print nat.
           Definition a := 1.
 
     The blank line after the directive is required.  If you begin a proof,
-    include an ``Abort`` afterwards to reset coqtop for the next example.
+    use the ``abort`` option to reset coqtop for the next example.
 
     Here is a list of permissible options:
 
-    - Display options
+    - Display options (choose exactly one)
 
       - ``all``: Display input and output
       - ``in``: Display only input
@@ -580,15 +580,17 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``undo``: Reset state after executing. Not compatible with ``reset``.
+      - ``fail``: Don't die if a command fails
+      - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
+      - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
     reST source file).  Use the ``reset`` option to reset Coq's state.
     """
     has_content = True
-    required_arguments = 0
-    optional_arguments = 1
+    required_arguments = 1
+    optional_arguments = 0
     final_argument_whitespace = True
     option_spec = { 'name': directives.unchanged }
     directive_name = "coqtop"
@@ -597,10 +599,8 @@ class CoqtopDirective(Directive):
         # Uses a ‘container’ instead of a ‘literal_block’ to disable
         # Pygments-based post-processing (we could also set rawsource to '')
         content = '\n'.join(self.content)
-        args = self.arguments[0].split() if self.arguments else ['in']
-        if 'all' in args:
-            args.extend(['in', 'out'])
-        node = nodes.container(content, coqtop_options = list(set(args)),
+        args = self.arguments[0].split()
+        node = nodes.container(content, coqtop_options = set(args),
                                classes=['coqtop', 'literal-block'])
         self.add_name(node)
         return [node]
@@ -827,22 +827,41 @@ class CoqtopBlocksTransform(Transform):
         return re.split(r"(?<=(?<!\.)\.)\s+", source)
 
     @staticmethod
-    def parse_options(options):
+    def parse_options(node):
         """Parse options according to the description in CoqtopDirective."""
-        opt_undo = 'undo' in options
+
+        options = node['coqtop_options']
+
+        # Behavior options
         opt_reset = 'reset' in options
-        opt_all, opt_none = 'all' in options, 'none' in options
-        opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options
+        opt_fail = 'fail' in options
+        opt_restart = 'restart' in options
+        opt_abort = 'abort' in options
+        options = options - set(('reset', 'fail', 'restart', 'abort'))
 
-        unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out')))
+        unexpected_options = list(options - set(('all', 'none', 'in', 'out')))
         if unexpected_options:
-            raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options))
-        elif (opt_input or opt_output) and opt_none:
-            raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’")
-        elif opt_reset and opt_undo:
-            raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’")
-
-        return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none
+            loc = get_node_location(node)
+            raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options))
+
+        # Display options
+        if len(options) != 1:
+            loc = get_node_location(node)
+            raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc))
+
+        opt_all = 'all' in options
+        opt_none = 'none' in options
+        opt_input = 'in' in options
+        opt_output = 'out' in options
+
+        return {
+            'reset': opt_reset,
+            'fail': opt_fail,
+            'restart': opt_restart,
+            'abort': opt_abort,
+            'input': opt_input or opt_all,
+            'output': opt_output or opt_all
+        }
 
     @staticmethod
     def block_classes(should_show, contents=None):
@@ -866,36 +885,59 @@ class CoqtopBlocksTransform(Transform):
                 blocks.append(re.sub("^", "    ", output, flags=re.MULTILINE) + "\n")
         return '\n'.join(blocks)
 
+    def add_coq_output_1(self, repl, node):
+        options = self.parse_options(node)
+
+        pairs = []
+
+        if options['restart']:
+            repl.sendone("Restart.")
+        if options['reset']:
+            repl.sendone("Reset Initial.")
+            repl.sendone("Set Coqtop Exit On Error.")
+        if options['fail']:
+            repl.sendone("Unset Coqtop Exit On Error.")
+        for sentence in self.split_sentences(node.rawsource):
+            pairs.append((sentence, repl.sendone(sentence)))
+        if options['abort']:
+            repl.sendone("Abort All.")
+        if options['fail']:
+            repl.sendone("Set Coqtop Exit On Error.")
+
+        dli = nodes.definition_list_item()
+        for sentence, output in pairs:
+            # Use Coqdoc to highlight input
+            in_chunks = highlight_using_coqdoc(sentence)
+            dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input']))
+            # Parse ANSI sequences to highlight output
+            out_chunks = AnsiColorsParser().colorize_str(output)
+            dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
+        node.clear()
+        node.rawsource = self.make_rawsource(pairs, options['input'], options['output'])
+        node['classes'].extend(self.block_classes(options['input'] or options['output']))
+        node += nodes.inline('', '', classes=['coqtop-reset'] * options['reset'])
+        node += nodes.definition_list(node.rawsource, dli)
+
     def add_coqtop_output(self):
         """Add coqtop's responses to a Sphinx AST
 
         Finds nodes to process using is_coqtop_block."""
         with CoqTop(color=True) as repl:
+            repl.sendone("Set Coqtop Exit On Error.")
             for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
-                options = node['coqtop_options']
-                opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options)
-
-                if opt_reset:
-                    repl.sendone("Reset Initial.")
-                pairs = []
-                for sentence in self.split_sentences(node.rawsource):
-                    pairs.append((sentence, repl.sendone(sentence)))
-                if opt_undo:
-                    repl.sendone("Undo {}.".format(len(pairs)))
-
-                dli = nodes.definition_list_item()
-                for sentence, output in pairs:
-                    # Use Coqdoq to highlight input
-                    in_chunks = highlight_using_coqdoc(sentence)
-                    dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input))
-                    # Parse ANSI sequences to highlight output
-                    out_chunks = AnsiColorsParser().colorize_str(output)
-                    dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output))
-                node.clear()
-                node.rawsource = self.make_rawsource(pairs, opt_input, opt_output)
-                node['classes'].extend(self.block_classes(opt_input or opt_output))
-                node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset)
-                node += nodes.definition_list(node.rawsource, dli)
+                try:
+                    self.add_coq_output_1(repl, node)
+                except CoqTopError as err:
+                    import textwrap
+                    MSG = ("{}: Error while sending the following to coqtop:\n{}" +
+                           "\n  coqtop output:\n{}" +
+                           "\n  Full error text:\n{}")
+                    indent = "    "
+                    loc = get_node_location(node)
+                    le = textwrap.indent(str(err.last_sentence), indent)
+                    bef = textwrap.indent(str(err.before), indent)
+                    fe = textwrap.indent(str(err.err), indent)
+                    raise ExtensionError(MSG.format(loc, le, bef, fe))
 
     @staticmethod
     def merge_coqtop_classes(kept_node, discarded_node):
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index 3ff00eaaf3..6d65d30d46 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -20,6 +20,14 @@ import re
 
 import pexpect
 
+
+class CoqTopError(Exception):
+    def __init__(self, err, last_sentence, before):
+        super().__init__()
+        self.err = err
+        self.before = before
+        self.last_sentence = last_sentence
+
 class CoqTop:
     """Create an instance of coqtop.
 
@@ -63,7 +71,7 @@ class CoqTop:
         self.coqtop.kill(9)
 
     def next_prompt(self):
-        "Wait for the next coqtop prompt, and return the output preceeding it."
+        """Wait for the next coqtop prompt, and return the output preceeding it."""
         self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
         return self.coqtop.before
 
@@ -75,13 +83,11 @@ class CoqTop:
         """
         # Suppress newlines, but not spaces: they are significant in notations
         sentence = re.sub(r"[\r\n]+", " ", sentence).strip()
-        self.coqtop.sendline(sentence)
         try:
+            self.coqtop.sendline(sentence)
             output = self.next_prompt()
-        except:
-            print("Error while sending the following sentence to coqtop: {}".format(sentence))
-            raise
-        # print("Got {}".format(repr(output)))
+        except Exception as err:
+            raise CoqTopError(err, sentence, self.coqtop.before)
         return output
 
 def sendmany(*sentences):
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e933f08735..1094fc86b4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -366,6 +366,11 @@ let top_goal_print ~doc c oldp newp =
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
 
+let exit_on_error =
+  let open Goptions in
+  declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"]
+    ~value:false
+
 let rec vernac_loop ~state =
   let open CAst in
   let open Vernac.State in
@@ -410,6 +415,7 @@ let rec vernac_loop ~state =
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+    if exit_on_error () then exit 1;
     vernac_loop ~state
 
 let rec loop ~state =