Merge PR #8064: Numeral notation (revisited again)

3 files changed, 14 insertions, 8 deletions

diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 117d6523a8..f8cedfff6e 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -23,7 +23,9 @@ Module Export Datatypes.
 
 Set Implicit Arguments.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
+Notation two := (S (S O)).
 
 Record prod (A B : Type) := pair { fst : A ; snd : B }.
 
@@ -159,7 +161,7 @@ End Adjointify.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),
@@ -220,12 +222,12 @@ Section ORecursion.
   Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o to O P == h o to O P)
   : g == h
-  := (fst (snd (extendable_to_O O 2) g h) p).1.
+  := (fst (snd (extendable_to_O O two) g h) p).1.
 
   Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P)
   : O_indpaths g h p (to O P x) = p x
-  := (fst (snd (extendable_to_O O 2) g h) p).2 x.
+  := (fst (snd (extendable_to_O O two) g h) p).2 x.
 
 End ORecursion.
 
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index c3e0da1117..fd2380a070 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Module Export Datatypes.
   Set Implicit Arguments.
   Notation nat := Coq.Init.Datatypes.nat.
+  Notation O := Coq.Init.Datatypes.O.
   Notation S := Coq.Init.Datatypes.S.
+  Notation one := (S O).
+  Notation two := (S one).
   Record prod (A B : Type) := pair { fst : A ; snd : B }.
   Notation "x * y" := (prod x y) : type_scope.
   Delimit Scope nat_scope with nat.
@@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l}
          (n : nat) {A : Type@{i}} {B : Type@{j}}
          (f : A -> B) (C : B -> Type@{k}) : Type@{l}
   := match n with
-     | 0 => Unit@{l}
+     | O => Unit@{l}
      | S n => (forall (g : forall a, C (f a)),
                   ExtensionAlong@{i j k l l} f C g) *
               forall (h k : forall b, C b),
@@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
     Definition O_rec {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q)
       : O P -> Q
-      := (fst (extendable_to_O O 1%nat) f).1.
+      := (fst (extendable_to_O O one) f).1.
 
     Definition O_rec_beta {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q) (x : P)
       : O_rec f (to O P x) = f x
-      := (fst (extendable_to_O O 1%nat) f).2 x.
+      := (fst (extendable_to_O O one) f).2 x.
 
     Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
                (g h : O P -> Q) (p : g o to O P == h o to O P)
       : g == h
-      := (fst (snd (extendable_to_O O 2) g h) p).1.
+      := (fst (snd (extendable_to_O O two) g h) p).1.
 
   End ORecursion.
 
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 4ad53bc629..13c47edc8f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
 Notation "x + y" := (sum x y) : type_scope.
 
@@ -449,7 +450,7 @@ Section Extensions.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),