Merge PR #9553: Sphinx various fixing of failing commands

Ack-by: Zimmi48

5 files changed, 49 insertions, 36 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
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