Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not Prelude.v

 Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v.
 This would now implies to make Datatypes.v depends on Decimal.v.
 Instead, we postpone the Numeral Notation for nat until Prelude.v,
 and we adapt those three tests that happen to live strictly between
 Datatypes and Prelude.

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),