Merge PR #9553: Sphinx various fixing of failing commands

Ack-by: Zimmi48

4 files changed, 45 insertions, 21 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)
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