From f1e54f2521bba13c59e89b4c06f2811866b5f92d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 12 Feb 2019 14:39:13 +0100
Subject: Increase sphinx recursion limit

Not sure why but it seems required for future commits.
---
 doc/sphinx/conf.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 912e363c9152012ecbff5272cded46e75a2f3c33 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 12 Feb 2019 14:39:43 +0100
Subject: Fix doc for coqtop:: undo

---
 doc/tools/coqrst/coqdomain.py | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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
-- 
cgit v1.2.3


From 146a9d73bd5ceff18e08d36d942dca874f388d5c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:42:56 +0100
Subject: Fix undefined SPHINX_DEPS when QUICK

---
 Makefile.doc | 1 +
 1 file changed, 1 insertion(+)

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
-- 
cgit v1.2.3


From f78d36363698f653ff8ff16389c58633579493eb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:45:10 +0100
Subject: Fix failing coqtops in extended-pattern-matching.rst

---
 doc/sphinx/addendum/extended-pattern-matching.rst | 28 +++++++++++++++--------
 1 file changed, 18 insertions(+), 10 deletions(-)

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
-- 
cgit v1.2.3


From d32a0db7b4d0775820b306badfe8072bd74cf62d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:51:08 +0100
Subject: Fix failing coqtops in generalized-rewriting.rst

---
 doc/sphinx/addendum/generalized-rewriting.rst | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

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).
-- 
cgit v1.2.3


From e5fb9c5cbce5e7e7e8fcb3d82c45074f9c165158 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:56:19 +0100
Subject: Fix failing coqtops in micromega.rst (the main one requires csdp)

Maybe we should still let it run but let's disable it until we install
csdp on the build server at least.
---
 doc/sphinx/addendum/micromega.rst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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.
-- 
cgit v1.2.3


From 75269e1b3fb98c8095b7f50e8ade2af87eb4061f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:15:21 +0100
Subject: Fix failing coqtops in ring.rst

---
 doc/sphinx/addendum/ring.rst | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

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
-- 
cgit v1.2.3


From 7104904f9f6e1a5e1b1590bd898ae20cb7178daf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:29:39 +0100
Subject: Fix failing coqtops universe-polymorphism.rst

---
 doc/sphinx/addendum/universe-polymorphism.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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
 
-- 
cgit v1.2.3


From f4621cc6774571efed498c58962b50bcaec12793 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:33:47 +0100
Subject: Fix failing coqtops in cic.rst

---
 doc/sphinx/language/cic.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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)
-- 
cgit v1.2.3


From d6f696465650cdbff0c8f09327e55d2013616a89 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:39:42 +0100
Subject: Fix failing coqtops in coq-library.rst

Mostly in the pattern

~~~
.. coqtop:: in

   Theorem foo : bla.
   Theorem bar : blah. (* nested proof error *)
~~~
---
 doc/sphinx/language/coq-library.rst | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

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:
-- 
cgit v1.2.3


From 123064557fce67e98f73ee56bb4aff534c9ceb85 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:43:12 +0100
Subject: Fix failing coqtops in gallina-extensions.rst

---
 doc/sphinx/language/gallina-extensions.rst | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

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
 
-- 
cgit v1.2.3


From aeb5deb414daf47e0f766489742b4ef9c2529c63 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 13:23:25 +0100
Subject: Fix failing coqtops in gallina-specification-language.rst

---
 .../language/gallina-specification-language.rst    | 26 +++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

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
-- 
cgit v1.2.3


From 2419d4539f469214b73c2c8f6d8fe2a6ccdfdb88 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 13:32:38 +0100
Subject: Fix failing coqtops in coqide.rst

---
 doc/sphinx/practical-tools/coqide.rst | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

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
-- 
cgit v1.2.3


From 669fe411aa6121809df686fd9de710b27a18fae2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 13:32:52 +0100
Subject: Fix failing coqtops in ltac.rst

---
 doc/sphinx/proof-engine/ltac.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3


From a9fbbfc53a7d7dcd5245960a0e3a2d2d7b6b8695 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 14:05:58 +0100
Subject: Fix failing coqtops in ssreflect-proof-language.rst

---
 .../proof-engine/ssreflect-proof-language.rst      | 192 +++++++++++----------
 1 file changed, 97 insertions(+), 95 deletions(-)

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.
-- 
cgit v1.2.3


From 68f3d842f6a9652cadf0698f54117fdc24172ac7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 14:14:04 +0100
Subject: Fix failing coqtops in tactics.rst

---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 081fef07b9..5788ae19e6 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
-- 
cgit v1.2.3


From d638148dc3e0220ac99761cf9f2efa8284882c41 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 14:14:16 +0100
Subject: Fix failing coqtops in syntax-extensions.rst

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

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.
-- 
cgit v1.2.3