Merge PR #9553: Sphinx various fixing of failing commands

Ack-by: Zimmi48

17 files changed, 217 insertions, 168 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 7ac710b8c9..4b2dd8ed4d 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -54,6 +54,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 doc: refman stdlib
 
+SPHINX_DEPS ?=
 ifndef QUICK
 SPHINX_DEPS := coq
 endif
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 7b8a86d1ab..d77690458d 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -59,7 +59,7 @@ pattern matching. Consider for example the function that computes the
 maximum of two natural numbers. We can write it in primitive syntax
 by:
 
-.. coqtop:: in undo
+.. coqtop:: in
 
    Fixpoint max (n m:nat) {struct m} : nat :=
      match n with
@@ -75,7 +75,7 @@ Multiple patterns
 
 Using multiple patterns in the definition of ``max`` lets us write:
 
-.. coqtop:: in undo
+.. coqtop:: in reset
 
    Fixpoint max (n m:nat) {struct m} : nat :=
        match n, m with
@@ -103,7 +103,7 @@ Aliasing subpatterns
 
 We can also use :n:`as @ident` to associate a name to a sub-pattern:
 
-.. coqtop:: in undo
+.. coqtop:: in reset
 
    Fixpoint max (n m:nat) {struct n} : nat :=
      match n, m with
@@ -128,18 +128,22 @@ Here is now an example of nested patterns:
 
 This is compiled into:
 
-.. coqtop:: all undo
+.. coqtop:: all
 
    Unset Printing Matching.
    Print even.
 
+.. coqtop:: none
+
+   Set Printing Matching.
+
 In the previous examples patterns do not conflict with, but sometimes
 it is comfortable to write patterns that admit a non trivial
 superposition. Consider the boolean function :g:`lef` that given two
 natural numbers yields :g:`true` if the first one is less or equal than the
 second one and :g:`false` otherwise. We can write it as follows:
 
-.. coqtop:: in undo
+.. coqtop:: in
 
    Fixpoint lef (n m:nat) {struct m} : bool :=
      match n, m with
@@ -158,7 +162,7 @@ is matched by the first pattern, and so :g:`(lef O O)` yields true.
 
 Another way to write this function is:
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Fixpoint lef (n m:nat) {struct m} : bool :=
      match n, m with
@@ -191,7 +195,7 @@ Multiple patterns that share the same right-hand-side can be
 factorized using the notation :n:`{+| @mult_pattern}`. For
 instance, :g:`max` can be rewritten as follows:
 
-.. coqtop:: in undo
+.. coqtop:: in reset
 
    Fixpoint max (n m:nat) {struct m} : nat :=
      match n, m with
@@ -269,7 +273,7 @@ When we use parameters in patterns there is an error message:
    Set Asymmetric Patterns.
    Check (fun l:List nat =>
      match l with
-     | nil => nil
+     | nil => nil _
      | cons _ l' => l'
      end).
    Unset Asymmetric Patterns.
@@ -325,7 +329,7 @@ Understanding dependencies in patterns
 
 We can define the function length over :g:`listn` by:
 
-.. coqtop:: in
+.. coqdoc::
 
    Definition length (n:nat) (l:listn n) := n.
 
@@ -367,6 +371,10 @@ different types and we need to provide the elimination predicate:
      | consn n' a y => consn (n' + m) a (concat n' y m l')
      end.
 
+.. coqtop:: none
+
+   Reset concat.
+
 The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`.
 In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr`
 are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`.
@@ -503,7 +511,7 @@ can also be caught in the matching.
 
 .. example::
 
-   .. coqtop:: in
+   .. coqtop:: in reset
 
       Inductive list : nat -> Set :=
       | nil : list 0
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index b606fb4dd2..cc788b3595 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -121,7 +121,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
    morphism parametric over ``A`` that respects the relation instance
    ``(set_eq A)``. The latter condition is proved by showing:
 
-   .. coqtop:: in
+   .. coqdoc::
 
      forall (A: Type) (S1 S1' S2 S2': list A),
        set_eq A S1 S1' ->
@@ -205,7 +205,7 @@ Adding new relations and morphisms
 
    For Leibniz equality, we may declare:
 
-   .. coqtop:: in
+   .. coqdoc::
 
      Add Parametric Relation (A : Type) : A (@eq A)
        [reflexivity proved by @refl_equal A]
@@ -274,7 +274,7 @@ following command.
    (maximally inserted) implicit arguments. If ``A`` is always set as
    maximally implicit in the previous example, one can write:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Add Parametric Relation A : (set A) eq_set
         reflexivity proved by eq_set_refl
@@ -282,13 +282,8 @@ following command.
         transitivity proved by eq_set_trans
         as eq_set_rel.
 
-   .. coqtop:: in
-
       Add Parametric Morphism A : (@union A) with
         signature eq_set ==> eq_set ==> eq_set as union_mor.
-
-   .. coqtop:: in
-
       Proof. exact (@union_compat A). Qed.
 
    We proceed now by proving a simple lemma performing a rewrite step and
@@ -300,7 +295,7 @@ following command.
    .. coqtop:: in
 
       Goal forall (S : set nat),
-        eq_set (union (union S empty) S) (union S S).
+        eq_set (union (union S (empty nat)) S) (union S S).
 
    .. coqtop:: in
 
@@ -486,7 +481,7 @@ registered as parametric relations and morphisms.
 
 .. example:: First class setoids
 
-   .. coqtop:: in
+   .. coqtop:: in reset
 
       Require Import Relation_Definitions Setoid.
 
@@ -623,6 +618,10 @@ declared as morphisms in the ``Classes.Morphisms_Prop`` module. For
 example, to declare that universal quantification is a morphism for
 logical equivalence:
 
+.. coqtop:: none
+
+   Require Import Morphisms.
+
 .. coqtop:: in
 
    Instance all_iff_morphism (A : Type) :
@@ -632,6 +631,10 @@ logical equivalence:
 
    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
@@ -650,7 +653,7 @@ functional arguments (or whatever subrelation of the pointwise
 extension). For example, one could declare the ``map`` combinator on lists
 as a morphism:
 
-.. coqtop:: in
+.. coqdoc::
 
    Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} :
             Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index b076aac1ed..e56b36caad 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -124,7 +124,7 @@ and checked to be :math:`-1`.
    that :tacn:`omega` does not solve, such as the following so-called *omega
    nightmare* :cite:`TheOmegaPaper`.
 
-.. coqtop:: in
+.. coqdoc::
 
    Goal forall x y,
      27 <= 11 * x + 13 * y <= 45 ->
@@ -234,7 +234,8 @@ proof by abstracting monomials by variables.
    To illustrate the working of the tactic, consider we wish to prove the
    following Coq goal:
 
-.. coqtop:: all
+.. needs csdp
+.. coqdoc::
 
    Require Import ZArith Psatz.
    Open Scope Z_scope.
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 8204d93fa7..20e4c6a3d6 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -197,7 +197,7 @@ be either Leibniz equality, or any relation declared as a setoid (see
 :ref:`tactics-enabled-on-user-provided-relations`).
 The definitions of ring and semiring (see module ``Ring_theory``) are:
 
-.. coqtop:: in
+.. coqdoc::
 
     Record ring_theory : Prop := mk_rt {
       Radd_0_l    : forall x, 0 + x == x;
@@ -235,7 +235,7 @@ coefficients could be the rational numbers, upon which the ring
 operations can be implemented. The fact that there exists a morphism
 is defined by the following properties:
 
-.. coqtop:: in 
+.. coqdoc::
 
     Record ring_morph : Prop := mkmorph {
       morph0    : [cO] == 0;
@@ -285,13 +285,14 @@ following property:
 
 .. coqtop:: in
 
+    Require Import Reals.
     Section POWER.
       Variable Cpow : Set.
       Variable Cp_phi : N -> Cpow.
       Variable rpow : R -> Cpow -> R.
     
       Record power_theory : Prop := mkpow_th {
-        rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
+        rpow_pow_N : forall r n, rpow r (Cp_phi n) = pow_N 1%R Rmult r n
       }.
     
     End POWER.
@@ -422,7 +423,7 @@ The interested reader is strongly advised to have a look at the
 file ``Ring_polynom.v``. Here a type for polynomials is defined:
 
 
-.. coqtop:: in
+.. coqdoc::
 
     Inductive PExpr : Type :=
       | PEc : C -> PExpr
@@ -437,7 +438,7 @@ file ``Ring_polynom.v``. Here a type for polynomials is defined:
 Polynomials in normal form are defined as:
 
 
-.. coqtop:: in
+.. coqdoc::
 
     Inductive Pol : Type :=
       | Pc : C -> Pol 
@@ -454,7 +455,7 @@ polynomial to an element of the concrete ring, and the second one that
 does the same for normal forms:
 
 
-.. coqtop:: in
+.. coqdoc::
 
 
     Definition PEeval : list R -> PExpr -> R := [...].
@@ -465,7 +466,7 @@ A function to normalize polynomials is defined, and the big theorem is
 its correctness w.r.t interpretation, that is:
 
 
-.. coqtop:: in
+.. coqdoc::
 
     Definition norm : PExpr -> Pol := [...].
     Lemma Pphi_dev_ok :
@@ -616,7 +617,7 @@ also supported. The equality can be either Leibniz equality, or any
 relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of
 fields and semifields is:
 
-.. coqtop:: in
+.. coqdoc::
 
     Record field_theory : Prop := mk_field {
       F_R : ring_theory rO rI radd rmul rsub ropp req;
@@ -636,7 +637,7 @@ fields and semifields is:
 The result of the normalization process is a fraction represented by
 the following type:
 
-.. coqtop:: in
+.. coqdoc::
 
     Record linear : Type := mk_linear {
       num : PExpr C;
@@ -690,7 +691,7 @@ for |Coq|’s type checker. Let us see why:
          x + 3 + y + y * z = x + 3 + y + z * y.
   intros; rewrite (Zmult_comm y z); reflexivity.
   Save foo.
-  Print  foo.
+  Print foo.
 
 At each step of rewriting, the whole context is duplicated in the
 proof term. Then, a tactic that does hundreds of rewriting generates
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 04aedd0cf6..6b10b7c0b3 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -223,7 +223,7 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
-Cumulative inductive types, coninductive types, variants and records
+Cumulative inductive types, coinductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the :g:`Cumulative` or
 :g:`NonCumulative` prefix in a monomorphic context.
@@ -236,11 +236,11 @@ Consider the following examples.
 
 .. coqtop:: all reset
 
-   Monomorphic Cumulative Inductive Unit := unit.
+   Fail Monomorphic Cumulative Inductive Unit := unit.
 
 .. coqtop:: all reset
 
-   Monomorphic NonCumulative Inductive Unit := unit.
+   Fail Monomorphic NonCumulative Inductive Unit := unit.
 
 .. coqtop:: all reset
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 39047f4f23..9d2afc080f 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -28,7 +28,7 @@ from shutil import copyfile
 import sphinx
 
 # Increase recursion limit for sphinx
-sys.setrecursionlimit(1500)
+sys.setrecursionlimit(3000)
 
 # If extensions (or modules to document with autodoc) are in another directory,
 # add these directories to sys.path here. If the directory is relative to the
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 962d2a94e3..a70cd4032d 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -782,7 +782,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort`
       Inductive even : nat -> Prop :=
       | even_O : even 0
       | even_S : forall n, odd n -> even (S n)
-      with odd : nat -> prop :=
+      with odd : nat -> Prop :=
       | odd_S : forall n, even n -> odd (S n).
 
 
@@ -929,7 +929,7 @@ condition* for a constant :math:`X` in the following cases:
 
       Inductive nattree (A:Type) : Type :=
       | leaf : nattree A
-      | node : A -> (nat -> nattree A) -> nattree A.
+      | natnode : A -> (nat -> nattree A) -> nattree A.
 
    Then every instantiated constructor of ``nattree A`` satisfies the nested positivity
    condition for ``nattree``:
@@ -939,7 +939,7 @@ condition* for a constant :math:`X` in the following cases:
      type of that constructor (primarily because ``nattree`` does not have any (real)
      arguments) ... (bullet 1)
 
-   + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the
+   + Type ``A → (nat → nattree A) → nattree A`` of constructor ``natnode`` satisfies the
      positivity condition for ``nattree`` because:
 
      - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1)
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index b82b3b0e80..963242ea72 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -146,7 +146,7 @@ Propositional Connectives
 
 First, we find propositional calculus connectives:
 
-.. coqtop:: in
+.. coqdoc::
 
   Inductive True : Prop := I.
   Inductive False :  Prop := .
@@ -236,7 +236,7 @@ Finally, a few easy lemmas are provided.
   single: eq_rect (term)
   single: eq_rect_r (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Theorem absurd : forall A C:Prop, A -> ~ A -> C.
   Section equality.
@@ -271,6 +271,10 @@ For instance ``f_equal3`` is defined the following way.
      (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
@@ -465,7 +469,7 @@ Intuitionistic Type Theory.
   single: Choice2 (term)
   single: bool_choice (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Lemma Choice :
    forall (S S':Set) (R:S -> S' -> Prop),
@@ -506,7 +510,7 @@ realizability interpretation.
   single: absurd_set (term)
   single: and_rect (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Definition except := False_rec.
   Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
@@ -531,7 +535,7 @@ section :tacn:`refine`). This scope is opened by default.
   The following example is not part of the standard library, but it
   shows the usage of the notations:
 
-  .. coqtop:: in
+  .. coqtop:: in reset
 
     Fixpoint even (n:nat) : bool :=
      match n with
@@ -558,7 +562,7 @@ section :tacn:`refine`). This scope is opened by default.
 
 Now comes the content of module ``Peano``:
 
-.. coqtop:: in
+.. coqdoc::
   
   Theorem eq_S : forall x y:nat, x = y -> S x = S y.
   Definition pred (n:nat) : nat :=
@@ -610,7 +614,7 @@ Finally, it gives the definition of the usual orderings ``le``,
 
   Inductive le (n:nat) : nat -> Prop :=
   | le_n : le n n
-  | le_S : forall m:nat, n <= m -> n <= (S m).
+  | le_S : forall m:nat, n <= m -> n <= (S m)
   where "n <= m" := (le n m) : nat_scope.
   Definition lt (n m:nat) := S n <= m.
   Definition ge (n m:nat) := m <= n.
@@ -625,7 +629,7 @@ induction principle.
   single: nat_case (term)
   single: nat_double_ind (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Theorem nat_case :
    forall (n:nat) (P:nat -> Prop), 
@@ -652,7 +656,7 @@ well-founded induction, in module ``Wf.v``.
    single: Acc_rect (term)
    single: well_founded (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Section Well_founded.
   Variable A : Type.
@@ -681,7 +685,7 @@ fixpoint equation can be proved.
   single: Fix_F_inv (term)
   single: Fix_F_eq (term)
 
-.. coqtop:: in
+.. coqdoc::
 
   Section FixPoint.
   Variable P : A -> Type.
@@ -715,7 +719,7 @@ of equality:
 .. coqtop:: in
 
    Inductive identity (A:Type) (a:A) : A -> Type :=
-     identity_refl : identity a a.
+     identity_refl : identity A a a.
 
 Some properties of ``identity`` are proved in the module ``Logic_Type``, which also
 provides the definition of ``Type`` level negation:
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 50a56f1d51..437b8e557e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1970,6 +1970,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          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.
@@ -2019,10 +2023,10 @@ or :g:`m` to the type :g:`nat` of natural numbers).
        Implicit Types m n : nat.
 
        Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m.
-
-       intros m n.
+       Proof. intros m n. Abort.
 
        Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
+       Abort.
 
 .. cmdv:: Implicit Type @ident : @type
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 5ecf007eff..9ab3f905e6 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -434,6 +434,10 @@ the identifier :g:`b` being used to represent the dependency.
    the return type. For instance, the following alternative definition is
    accepted and has the same meaning as the previous one.
 
+   .. coqtop:: none
+
+      Reset bool_case.
+
    .. coqtop:: in
 
       Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) :=
@@ -471,7 +475,7 @@ For instance, in the following example:
 
    Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
    match H in eq _ _ z return eq A z x with
-   | eq_refl _ => eq_refl A x
+   | eq_refl _ _ => eq_refl A x
    end.
 
 the type of the branch is :g:`eq A x x` because the third argument of
@@ -826,6 +830,10 @@ Simple inductive types
 
       .. example::
 
+         .. coqtop:: none
+
+            Reset nat.
+
          .. coqtop:: in
 
             Inductive nat : Set := O | S (_:nat).
@@ -904,6 +912,10 @@ Parametrized inductive types
       Once again, it is possible to specify only the type of the arguments
       of the constructors, and to omit the type of the conclusion:
 
+      .. coqtop:: none
+
+         Reset list.
+
       .. coqtop:: in
 
          Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
@@ -949,7 +961,7 @@ Parametrized inductive types
      inductive definitions are abstracted over their parameters
      before type checking constructors, allowing to write:
 
-     .. coqtop:: all undo
+     .. coqtop:: all
 
         Set Uniform Inductive Parameters.
         Inductive list3 (A:Set) : Set :=
@@ -960,7 +972,7 @@ Parametrized inductive types
      and using :cmd:`Context` to give the uniform parameters, like so
      (cf. :ref:`section-mechanism`):
 
-     .. coqtop:: all undo
+     .. coqtop:: all reset
 
         Section list3.
         Context (A:Set).
@@ -1038,7 +1050,7 @@ Mutually defined inductive types
    two type variables :g:`A` and :g:`B`, the declaration should be
    done the following way:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B
 
@@ -1130,6 +1142,10 @@ found in e.g. Agda, and preserves subject reduction.
 
 The above example can be rewritten in the following way.
 
+.. coqtop:: none
+
+   Reset Stream.
+
 .. coqtop:: all
 
    Set Primitive Projections.
@@ -1147,7 +1163,7 @@ axiom.
 
 .. coqtop:: all
 
-   Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s).
+   Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
 
 More generally, as in the case of positive coinductive types, it is consistent
 to further identify extensional equality of coinductive types with propositional
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 9455228e7d..8b7fe20191 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -230,10 +230,12 @@ mathematical symbols ∀ and ∃, you may define:
 
 .. coqtop:: in
 
-  Notation "∀ x : T, P" :=
-  (forall x : T, P) (at level 200, x ident).
-  Notation "∃ x : T, P" :=
-  (exists x : T, P) (at level 200, x ident).
+   Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+     (at level 200, x binder, y binder, right associativity)
+     : type_scope.
+   Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
+     (at level 200, x binder, y binder, right associativity)
+     : type_scope.
 
 There exists a small set of such notations already defined, in the
 file `utf8.v` of Coq library, so you may enable them just by
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 442077616f..4f486a777d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -859,6 +859,10 @@ 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,6 +1030,10 @@ Counting the goals
 
          all:pr_numgoals.
 
+      .. coqtop:: none
+
+         Abort.
+
 Testing boolean expressions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 483dbd311d..ec97377128 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -233,7 +233,7 @@ construct differs from the latter in that
 
     .. coqtop:: reset all
 
-       Definition f u := let (m, n) := u in m + n.
+       Fail Definition f u := let (m, n) := u in m + n.
 
 
 The ``let:`` construct is just (more legible) notation for the primitive
@@ -413,7 +413,7 @@ each point of use, e.g., the above definition can be written:
      Variable all : (T -> bool) -> list T -> bool.
 
 
-  .. coqtop:: all undo
+  .. coqtop:: all
 
      Prenex Implicits null.
      Definition all_null (s : list T) := all null s.
@@ -436,7 +436,7 @@ The syntax of the new declaration is
    a ``Set Printing All`` command). All |SSR| library files thus start
    with the incantation
 
-   .. coqtop:: all undo
+   .. coqdoc::
 
       Set Implicit Arguments.
       Unset Strict Implicit.
@@ -505,7 +505,7 @@ Definitions
    |SSR| pose tactic supports *open syntax*: the body of the
    definition does not need surrounding parentheses. For instance:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose t := x + y.
 
@@ -534,7 +534,7 @@ The |SSR| pose tactic also supports (co)fixpoints, by providing
 the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …``
 constructs. For instance, the following tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose fix f (x y : nat) {struct x} : nat :=
      if x is S p then S (f p y) else 0.
@@ -544,7 +544,7 @@ on natural numbers.
 
 Similarly, local cofixpoints can be defined by a tactic of the form:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose cofix f (arg : T) := … .
 
@@ -553,26 +553,26 @@ offers a smooth way of defining local abstractions. The type of
 “holes” is guessed by type inference, and the holes are abstracted.
 For instance the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f := _ + 1.
 
 is shorthand for:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f n := n + 1.
 
 When the local definition of a function involves both arguments and
 holes, hole abstractions appear first. For instance, the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f x := x + _.
 
 is shorthand for:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f n x := x + n.
 
@@ -580,13 +580,13 @@ The interaction of the pose tactic with the interpretation of implicit
 arguments results in a powerful and concise syntax for local
 definitions involving dependent types. For instance, the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f x y := (x, y).
 
 adds to the context the local definition:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y).
 
@@ -766,7 +766,7 @@ Moreover:
      .. coqtop:: all
 
         Lemma test : forall x : nat, x + 1 = 0.
-        set t := _ + 1.
+        Fail set t := _ + 1.
 
 + Typeclass inference should fill in any residual hole, but matching
   should never assign a value to a global existential variable.
@@ -889,7 +889,7 @@ only one occurrence of the selected term.
      .. coqtop:: all
 
         Lemma test x y z : (x + y) + (z + z) = z + z.
-        set a := {2}(_ + _).
+        Fail set a := {2}(_ + _).
 
 
 .. _basic_localization_ssr:
@@ -1079,7 +1079,7 @@ constants to the goal.
 
 Because they are tacticals, ``:`` and ``=>`` can be combined, as in
 
-.. coqtop:: in
+.. coqdoc::
 
    move: m le_n_m => p le_n_p.
 
@@ -1139,7 +1139,7 @@ Basic tactics like apply and elim can also be used without the ’:’
 tactical: for example we can directly start a proof of ``subnK`` by
 induction on the top variable ``m`` with
 
-.. coqtop:: in
+.. coqdoc::
 
    elim=> [|m IHm] n le_n.
 
@@ -1150,7 +1150,7 @@ explained in terms of the goal stack::
 
 is basically equivalent to
 
-.. coqtop:: in
+.. coqdoc::
 
    move: a H1 H2; tactic => a H1 H2.
 
@@ -1163,13 +1163,13 @@ temporary abbreviation to hide the statement of the goal from
 The general form of the in tactical can be used directly with the
 ``move``, ``case`` and ``elim`` tactics, so that one can write
 
-.. coqtop:: in
+.. coqdoc::
 
    elim: n => [|n IHn] in m le_n_m *.
 
 instead of
 
-.. coqtop:: in
+.. coqdoc::
 
    elim: n m le_n_m => [|n IHn] m le_n_m.
 
@@ -1398,7 +1398,7 @@ Switches affect the discharging of a :token:`d_item` as follows:
 
 For example, the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    move: n {2}n (refl_equal n).
 
@@ -1409,7 +1409,7 @@ For example, the tactic:
 
 Therefore this tactic changes any goal ``G`` into
 
-.. coqtop::
+.. coqdoc::
 
    forall n n0 : nat, n = n0 -> G.
 
@@ -1843,7 +1843,7 @@ Generation of equations
 The generation of named equations option stores the definition of a
 new constant as an equation. The tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    move En: (size l) => n.
 
@@ -1851,7 +1851,7 @@ where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and
 adds the fact ``En : size l = n`` to the context.
 This is quite different from:
 
-.. coqtop:: in
+.. coqdoc::
 
    pose n := (size l).
 
@@ -1936,7 +1936,7 @@ be substituted.
    inferred looking at the type of the top assumption. This allows for the
    compact syntax:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       case: {2}_ / eqP.
 
@@ -2112,7 +2112,7 @@ In the script provided as example in section :ref:`indentation_ssr`, the
 paragraph corresponding to each sub-case ends with a tactic line prefixed
 with a ``by``, like in:
 
-.. coqtop:: in
+.. coqdoc::
 
    by apply/eqP; rewrite -dvdn1.
 
@@ -2147,13 +2147,13 @@ A natural and common way of closing a goal is to apply a lemma which
 is the exact one needed for the goal to be solved. The defective form
 of the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    exact.
 
 is equivalent to:
 
-.. coqtop:: in
+.. coqdoc::
 
    do [done | by move=> top; apply top].
 
@@ -2161,13 +2161,13 @@ where ``top`` is a fresh name assigned to the top assumption of the goal.
 This applied form is supported by the ``:`` discharge tactical, and the
 tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    exact: MyLemma.
 
 is equivalent to:
 
-.. coqtop:: in
+.. coqdoc::
 
    by apply: MyLemma.
 
@@ -2179,19 +2179,19 @@ is equivalent to:
    follows the ``by`` keyword is considered to be a parenthesized block applied to
    the current goal. Hence for example if the tactic:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       by rewrite my_lemma1.
 
    succeeds, then the tactic:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       by rewrite my_lemma1; apply my_lemma2.
 
    usually fails since it is equivalent to:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       by (rewrite my_lemma1; apply my_lemma2).
 
@@ -2247,7 +2247,7 @@ Finally, the tactics ``last`` and ``first`` combine with the branching syntax
 of Ltac: if the tactic generates n subgoals on a given goal,
 then the tactic
 
-.. coqtop:: in
+.. coqdoc::
 
    tactic ; last k [ tactic1 |…| tacticm ] || tacticn.
 
@@ -2262,7 +2262,6 @@ to the others.
 
    .. coqtop:: reset
 
-      Abort.
       From Coq Require Import ssreflect.
       Set Implicit Arguments.
       Unset Strict Implicit.
@@ -2296,13 +2295,13 @@ Iteration
 
 A tactic of the form:
 
-.. coqtop:: in
+.. coqdoc::
 
    do [ tactic 1 | … | tactic n ].
 
 is equivalent to the standard Ltac expression:
 
-.. coqtop:: in
+.. coqdoc::
 
    first [ tactic 1 | … | tactic n ].
 
@@ -2327,14 +2326,14 @@ Their meaning is:
 
 For instance, the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    tactic; do 1? rewrite mult_comm.
 
 rewrites at most one time the lemma ``mult_comm`` in all the subgoals
 generated by tactic , whereas the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    tactic; do 2! rewrite mult_comm.
 
@@ -2518,7 +2517,7 @@ tactics of the form:
 
 which behave like:
 
-.. coqtop:: in
+.. coqdoc::
 
    have: term ; first by tactic.
    move=> clear_switch i_item.
@@ -2531,7 +2530,7 @@ to introduce the new assumption itself.
 The ``by`` feature is especially convenient when the proof script of the
 statement is very short, basically when it fits in one line like in:
 
-.. coqtop:: in
+.. coqdoc::
 
    have H23 : 3 + 2 = 2 + 3 by rewrite addnC.
 
@@ -2559,7 +2558,7 @@ the further use of the intermediate step. For instance,
 Thanks to the deferred execution of clears, the following idiom is
 also supported (assuming x occurs in the goal only):
 
-.. coqtop:: in
+.. coqdoc::
 
    have {x} -> : x = y.
 
@@ -2635,7 +2634,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:
 
-.. coqtop:: in
+.. coqdoc::
 
    have (x) : 2 * x = x + x by omega.
 
@@ -2816,7 +2815,7 @@ The
 + but the optional clear item is still performed in the *second*
   branch. This means that the tactic:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      suff {H} H : forall x : nat, x >= 0.
 
@@ -2888,7 +2887,7 @@ name of the local definition with the ``@`` character.
 
 In the second subgoal, the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    move=> clear_switch i_item.
 
@@ -2995,10 +2994,13 @@ illustrated in the following example.
   the pattern ``id (addx x)``, that would produce the following first
   subgoal
 
-  .. coqtop:: none
+  .. coqtop:: none reset
+
+     From Coq Require Import ssreflect Omega.
+     Set Implicit Arguments.
+     Unset Strict Implicit.
+     Unset Printing Implicit Defensive.
 
-     Abort All.
-     From Coq Require Import Omega.
      Section Test.
      Variable x : nat.
      Definition addx z := z + x.
@@ -3153,7 +3155,7 @@ An :token:`r_item` can be:
 
         Definition f := fun x y => x + y.
         Lemma test x y : x + y = f y x.
-        rewrite -[f y]/(y + _).
+        Fail rewrite -[f y]/(y + _).
 
      but the following script succeeds
 
@@ -3192,7 +3194,7 @@ tactics.
 
 In a rewrite tactic of the form:
 
-.. coqtop:: in
+.. coqdoc::
 
    rewrite occ_switch [term1]term2.
 
@@ -3235,7 +3237,7 @@ Performing rewrite and simplification operations in a single tactic
 enhances significantly the concision of scripts. For instance the
 tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    rewrite /my_def {2}[f _]/= my_eq //=.
 
@@ -3316,7 +3318,7 @@ the equality.
   .. coqtop:: all
 
      Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0.
-     rewrite [x + _]H.
+     Fail rewrite [x + _]H.
 
   Indeed the left hand side of ``H`` does not match
   the redex identified by the pattern ``x + y * 4``.
@@ -3498,7 +3500,7 @@ reasoning purposes. The library also provides one lemma per such
 operation, stating that both versions return the same values when
 applied to the same arguments:
 
-.. coqtop:: in
+.. coqdoc::
 
      Lemma addE : add =2 addn.
      Lemma doubleE : double =1 doublen.
@@ -3514,7 +3516,7 @@ hand side. In order to reason conveniently on expressions involving
 the efficient operations, we gather all these rules in the definition
 ``trecE``:
 
-.. coqtop:: in
+.. coqdoc::
 
    Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
 
@@ -3572,14 +3574,14 @@ cases:
 
 + |SSR| never accepts to rewrite indeterminate patterns like:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      Lemma foo (x : unit) : x = tt.
 
   |SSR| will however accept the
   ηζ expansion of this rule:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      Lemma fubar (x : unit) : (let u := x in u) = tt.
 
@@ -3617,7 +3619,7 @@ cases:
 
     .. coqtop:: all
 
-       rewrite H.
+       Fail rewrite H.
 
     Rewriting with ``H`` first requires unfolding the occurrences of
     ``f``
@@ -3729,7 +3731,7 @@ copy of any term t. However this copy is (on purpose) *not
 convertible* to t in the |Coq| system [#8]_. The job is done by the
 following construction:
 
-.. coqtop:: in
+.. coqdoc::
 
    Lemma master_key : unit. Proof. exact tt. Qed.
    Definition locked A := let: tt := master_key in fun x : A => x.
@@ -3793,14 +3795,14 @@ some functions by the partial evaluation switch ``/=``, unless this
 allowed the evaluation of a condition. This is possible thanks to another
 mechanism of term tagging, resting on the following *Notation*:
 
-.. coqtop:: in
+.. coqdoc::
 
    Notation "'nosimpl' t" := (let: tt := tt in t).
 
 The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition.
 More precisely, given:
 
-.. coqtop:: in
+.. coqdoc::
 
    Definition foo := (nosimpl bar).
 
@@ -3816,7 +3818,7 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to
    The ``nosimpl`` trick only works if no reduction is apparent in
    ``t``; in particular, the declaration:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Definition foo x := nosimpl (bar x).
 
@@ -3824,14 +3826,14 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to
    function, and to use the following definition, which blocks the
    reduction as expected:
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Definition foo x := nosimpl bar x.
 
 A standard example making this technique shine is the case of
 arithmetic operations. We define for instance:
 
-.. coqtop:: in
+.. coqdoc::
 
    Definition addn := nosimpl plus.
 
@@ -3851,7 +3853,7 @@ Congruence
 Because of the way matching interferes with parameters of type families,
 the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    apply: my_congr_property.
 
@@ -4047,7 +4049,7 @@ For a quick glance at what can be expressed with the last
 :token:`r_pattern`
 consider the goal ``a = b`` and the tactic
 
-.. coqtop:: in
+.. coqdoc::
 
    rewrite [in X in _ = X]rule.
 
@@ -4148,14 +4150,14 @@ patterns over simple terms, but to interpret a pattern with double
 parentheses as a simple term. For example, the following tactic would
 capture any occurrence of the term ``a in A``.
 
-.. coqtop:: in
+.. coqdoc::
 
    set t := ((a in A)).
 
 Contextual patterns can also be used as arguments of the ``:`` tactical.
 For example:
 
-.. coqtop:: in
+.. coqdoc::
 
    elim: n (n in _ = n) (refl_equal n).
 
@@ -4246,7 +4248,7 @@ context shortcuts.
 The following example is taken from ``ssreflect.v`` where the
 ``LHS`` and ``RHS`` shortcuts are defined.
 
-.. coqtop:: in
+.. coqdoc::
 
    Notation RHS := (X in _ = X)%pattern.
    Notation LHS := (X in X = _)%pattern.
@@ -4254,7 +4256,7 @@ The following example is taken from ``ssreflect.v`` where the
 Shortcuts defined this way can be freely used in place of the trailing
 ``ident in term`` part of any contextual pattern. Some examples follow:
 
-.. coqtop:: in
+.. coqdoc::
 
    set rhs := RHS.
    rewrite [in RHS]rule.
@@ -4287,13 +4289,13 @@ The view syntax combined with the ``elim`` tactic specifies an elimination
 scheme to be used instead of the default, generated, one. Hence the
 |SSR| tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    elim/V.
 
 is a synonym for:
 
-.. coqtop:: in
+.. coqdoc::
 
    intro top; elim top using V; clear top.
 
@@ -4303,13 +4305,13 @@ Since an elimination view supports the two bookkeeping tacticals of
 discharge and introduction (see section :ref:`basic_tactics_ssr`),
 the |SSR| tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    elim/V: x => y.
 
 is a synonym for:
 
-.. coqtop:: in
+.. coqdoc::
 
    elim x using V; clear x; intro y.
 
@@ -4367,13 +4369,13 @@ command) can be combined with the type family switches described
 in section :ref:`type_families_ssr`.
 Consider an eliminator ``foo_ind`` of type:
 
-.. coqtop:: in
+.. coqdoc::
 
    foo_ind : forall …, forall x : T, P p1 … pm.
 
 and consider the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    elim/foo_ind: e1 … / en.
 
@@ -4424,7 +4426,7 @@ Here is an example of a regular, but nontrivial, eliminator.
   The following tactics are all valid and perform the same elimination
   on this goal.
 
-  .. coqtop:: in
+  .. coqdoc::
 
      elim/plus_ind: z / (plus _ z).
      elim/plus_ind: {z}(plus _ z).
@@ -4473,7 +4475,7 @@ Here is an example of a regular, but nontrivial, eliminator.
 
   .. coqtop:: all
 
-     elim/plus_ind: y / _.
+     Fail elim/plus_ind: y / _.
 
   triggers an error: in the conclusion
   of the ``plus_ind`` eliminator, the first argument of the predicate
@@ -4494,7 +4496,7 @@ Here is an example of a truncated eliminator:
      Unset Printing Implicit Defensive.
      Section Test.
 
-  .. coqtop:: in
+  .. coqdoc::
 
      Lemma test p n (n_gt0 : 0 < n) (pr_p : prime p) :
        p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 ->
@@ -4505,7 +4507,7 @@ Here is an example of a truncated eliminator:
 
   where the type of the ``big_prop`` eliminator is
 
-  .. coqtop:: in
+  .. coqdoc::
 
      big_prop: forall (R : Type) (Pb : R -> Type)
        (idx : R) (op1 : R -> R -> R), Pb idx ->
@@ -4518,7 +4520,7 @@ Here is an example of a truncated eliminator:
   inferred one is used instead: ``big[_/_]_(i <- _ | _ i) _ i``,
   and after the introductions, the following goals are generated:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      subgoal 1 is:
        p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1
@@ -4624,7 +4626,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss
 
   This view tactic performs:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb].
 
@@ -4661,14 +4663,14 @@ relevant for the current goal.
   the double implication into the expected simple implication. The last
   script is in fact equivalent to:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      Lemma test a b : P (a || b) -> True.
      move/(iffLR (PQequiv _ _)).
 
   where:
 
-  .. coqtop:: in
+  .. coqdoc::
 
      Lemma iffLR P Q : (P <-> Q) -> P -> Q.
 
@@ -4810,7 +4812,7 @@ decidable predicate to its boolean version.
 First, booleans are injected into propositions using the coercion
 mechanism:
 
-.. coqtop:: in
+.. coqdoc::
 
    Coercion is_true (b : bool) := b = true.
 
@@ -4827,7 +4829,7 @@ To get all the benefits of the boolean reflection, it is in fact
 convenient to introduce the following inductive predicate ``reflect`` to
 relate propositions and booleans:
 
-.. coqtop:: in
+.. coqdoc::
 
    Inductive reflect (P: Prop): bool -> Type :=
    | Reflect_true : P -> reflect P true
@@ -4838,7 +4840,7 @@ logically equivalent propositions.
 
 For instance, the following lemma:
 
-.. coqtop:: in
+.. coqdoc::
 
      Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2).
 
@@ -4853,20 +4855,20 @@ to the case analysis of |Coq|’s inductive types.
 
 Since the equivalence predicate is defined in |Coq| as:
 
-.. coqtop:: in
+.. coqdoc::
 
    Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
 
 where ``/\`` is a notation for ``and``:
 
-.. coqtop:: in
+.. coqdoc::
 
    Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B.
 
 This make case analysis very different according to the way an
 equivalence property has been defined.
 
-.. coqtop:: in
+.. coqdoc::
 
    Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2).
 
@@ -4950,13 +4952,13 @@ Specializing assumptions
 
 The |SSR| tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    move/(_ term1 … termn).
 
 is equivalent to the tactic:
 
-.. coqtop:: in
+.. coqdoc::
 
    intro top; generalize (top term1 … termn); clear top.
 
@@ -5013,13 +5015,13 @@ If ``term`` is a double implication, then the view hint will be one of
 the defined view hints for implication. These hints are by default the
 ones present in the file ``ssreflect.v``:
 
-.. coqtop:: in
+.. coqdoc::
 
    Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q.
 
 which transforms a double implication into the left-to-right one, or:
 
-.. coqtop:: in
+.. coqdoc::
 
    Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P.
 
@@ -5123,7 +5125,7 @@ equality, while the second term is the one applied to the right hand side.
 
 In this context, the identity view can be used when no view has to be applied:
 
-.. coqtop:: in
+.. coqdoc::
 
    Lemma idP : reflect b1 b1.
 
@@ -5198,7 +5200,7 @@ in sequence. Both move and apply can be followed by an arbitrary
 number of ``/term``. The main difference between the following two
 tactics
 
-.. coqtop:: in
+.. coqdoc::
 
    apply/v1/v2/v3.
    apply/v1; apply/v2; apply/v3.
@@ -5210,7 +5212,7 @@ line would apply the view ``v2`` to all the goals generated by ``apply/v1``.
 Note that the NO-OP intro pattern ``-`` can be used to separate two views,
 making the two following examples equivalent:
 
-.. coqtop:: in
+.. coqdoc::
 
    move=> /v1; move=> /v2.
    move=> /v1 - /v2.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 66d510bc0e..0bcfce2322 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2493,7 +2493,7 @@ and an explanation of the underlying technique.
    Let us consider the relation Le over natural numbers and the following
    variables:
 
-   .. coqtop:: all
+   .. coqtop:: all reset
 
       Inductive Le : nat -> nat -> Set :=
       | LeO : forall n:nat, Le 0 n
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 105b0445fd..4f46a80dcf 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -181,7 +181,7 @@ rules. Some simple left factorization work has to be done. Here is an example.
 .. coqtop:: all
 
    Notation "x < y" := (lt x y) (at level 70).
-   Notation "x < y < z" := (x < y /\ y < z) (at level 70).
+   Fail Notation "x < y < z" := (x < y /\ y < z) (at level 70).
 
 In order to factorize the left part of the rules, the subexpression
 referred to by ``y`` has to be at the same level in both rules. However the
@@ -486,7 +486,7 @@ Sometimes, for the sake of factorization of rules, a binder has to be
 parsed as a term. This is typically the case for a notation such as
 the following:
 
-.. coqtop:: in
+.. coqdoc::
 
    Notation "{ x : A | P }" := (sig (fun x : A => P))
        (at level 0, x at level 99 as ident).
@@ -788,9 +788,9 @@ main grammar, or from another custom entry as is the case in
 to indicate that ``e`` has to be parsed at level ``2`` of the grammar
 associated to the custom entry ``expr``. The level can be omitted, as in
 
-.. coqtop:: in
+.. coqdoc::
 
-   Notation "[ e ]" := e (e custom expr)`.
+   Notation "[ e ]" := e (e custom expr).
 
 in which case Coq tries to infer it.
 
@@ -1058,7 +1058,7 @@ Binding arguments of a constant to an interpretation scope
    in the scope delimited by the key ``F`` (``Rfun_scope``) and the last
    argument in the scope delimited by the key ``R`` (``R_scope``).
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Arguments plus_fct (f1 f2)%F x%R.
 
@@ -1066,7 +1066,7 @@ Binding arguments of a constant to an interpretation scope
    parentheses. In the following example arguments A and B are marked as
    maximally inserted implicit arguments and are put into the type_scope scope.
 
-   .. coqtop:: in
+   .. coqdoc::
 
       Arguments respectful {A B}%type (R R')%signature _ _.
 
@@ -1148,7 +1148,7 @@ Binding types of arguments to an interpretation scope
    can be bound to an interpretation scope. The command to do it is
    :n:`Bind Scope @scope with @class`
 
-   .. coqtop:: in
+   .. coqtop:: in reset
 
       Parameter U : Set.
       Bind Scope U_scope with U.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 067af954ad..0dd9b3aa3e 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -560,7 +560,7 @@ class CoqtopDirective(Directive):
 
     Example::
 
-       .. coqtop:: in reset undo
+       .. coqtop:: in undo
 
           Print nat.
           Definition a := 1.
@@ -580,8 +580,7 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
-        running all the commands in this block
+      - ``undo``: Reset state after executing. Not compatible with ``reset``.
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per