Renaming Numeral.v into Number.v

9 files changed, 114 insertions, 114 deletions

diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6dadd8c7fe..84913abcdc 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -124,7 +124,7 @@ Check r 2 3.
 End I.
 
 Require Import Coq.Numbers.Cyclic.Int63.Int63.
-Module NumeralNotations.
+Module NumberNotations.
   Module Test17.
     (** Test int63 *)
     Declare Scope test17_scope.
@@ -134,7 +134,7 @@ Module NumeralNotations.
     Number Notation myint63 of_int to_int : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
-End NumeralNotations.
+End NumberNotations.
 
 Module K.
 
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 8065c8d311..b00fd3b485 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -1,9 +1,9 @@
 The command has indeed failed with message:
-Unexpected term (nat -> nat) while parsing a numeral notation.
+Unexpected term (nat -> nat) while parsing a number notation.
 The command has indeed failed with message:
-Unexpected non-option term opaque4 while parsing a numeral notation.
+Unexpected non-option term opaque4 while parsing a number notation.
 The command has indeed failed with message:
-Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral
+Unexpected term (fun (A : Type) (x : A) => x) while parsing a number
 notation.
 let v := 0%ppp in v : punit
      : punit
@@ -32,7 +32,7 @@ Warning: To avoid stack overflow, large numbers in punit are interpreted as
 applications of pto_punits. [abstract-large-number,numbers]
 The command has indeed failed with message:
 In environment
-v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit
+v := pto_punits (Number.UIntDec (Decimal.D1 Decimal.Nil)) : punit
 The term "v" has type "punit@{Set}" while it is expected to have type
  "punit@{u}".
 S
@@ -61,7 +61,7 @@ The command has indeed failed with message:
 In environment
 v := 0 : nat
 The term "v" has type "nat" while it is expected to have type "wuint".
-     = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |}
+     = {| unwrap := Number.UIntDec (Decimal.D0 Decimal.Nil) |}
      : wuint
 let v := 0%wuint8' in v : wuint
      : wuint
@@ -82,7 +82,7 @@ function (of_uint) targets an option type.
 The command has indeed failed with message:
 The 'abstract after' directive has no effect when the parsing function
 (of_uint) targets an option type. [abstract-large-number-no-op,numbers]
-let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit
+let v := of_uint (Number.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit
      : unit
 let v := 0%test13 in v : unit
      : unit
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index e411005da3..af0aa895d1 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -5,17 +5,17 @@ Declare Scope opaque_scope.
 (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
 Module Test1.
   Axiom hold : forall {A B C}, A -> B -> C.
-  Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
-  Number Notation Numeral.int opaque3 opaque3 : opaque_scope.
+  Definition opaque3 (x : Number.int) : Number.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
+  Number Notation Number.int opaque3 opaque3 : opaque_scope.
   Delimit Scope opaque_scope with opaque.
   Fail Check 1%opaque.
 End Test1.
 
 (* https://github.com/coq/coq/pull/8064#discussion_r202497990 *)
 Module Test2.
-  Axiom opaque4 : option Numeral.int.
-  Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4.
-  Number Notation Numeral.int opaque6 opaque6 : opaque_scope.
+  Axiom opaque4 : option Number.int.
+  Definition opaque6 (x : Number.int) : option Number.int := opaque4.
+  Number Notation Number.int opaque6 opaque6 : opaque_scope.
   Delimit Scope opaque_scope with opaque.
   Open Scope opaque_scope.
   Fail Check 1%opaque.
@@ -24,8 +24,8 @@ End Test2.
 Declare Scope silly_scope.
 
 Module Test3.
-  Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A).
-  Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x).
+  Inductive silly := SILLY (v : Number.uint) (f : forall A, A -> A).
+  Definition to_silly (v : Number.uint) := SILLY v (fun _ x => x).
   Definition of_silly (v : silly) := match v with SILLY v _ => v end.
   Number Notation silly to_silly of_silly : silly_scope.
   Delimit Scope silly_scope with silly.
@@ -45,15 +45,15 @@ Module Test4.
   Declare Scope upp.
   Declare Scope ppps.
   Polymorphic NonCumulative Inductive punit := ptt.
-  Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
-  Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt.
-  Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0.
-  Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
-  Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0.
-  Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
-  Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
-  Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
-  Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
+  Polymorphic Definition pto_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pto_punit_all (v : Number.uint) : punit := ptt.
+  Polymorphic Definition pof_punit (v : punit) : Number.uint := Nat.to_num_uint 0.
+  Definition to_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Definition of_punit (v : punit) : Number.uint := Nat.to_num_uint 0.
+  Polymorphic Definition pto_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Polymorphic Definition pof_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
+  Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
   Number Notation punit to_punit of_punit : pto.
   Number Notation punit pto_punit of_punit : ppo.
   Number Notation punit to_punit pof_punit : ptp.
@@ -96,7 +96,7 @@ Module Test5.
 End Test5.
 
 Module Test6.
-  (* Check that numeral notations on enormous terms don't take forever to print/parse *)
+  (* Check that number notations on enormous terms don't take forever to print/parse *)
   (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *)
   Fixpoint ack (n m : nat) : nat :=
     match n with
@@ -113,8 +113,8 @@ Module Test6.
 
   Local Set Primitive Projections.
   Record > wnat := wrap { unwrap :> nat }.
-  Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x.
-  Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x.
+  Definition to_uint (x : wnat) : Number.uint := Nat.to_num_uint x.
+  Definition of_uint (x : Number.uint) : wnat := Nat.of_num_uint x.
   Module Export Scopes.
     Declare Scope wnat_scope.
     Delimit Scope wnat_scope with wnat.
@@ -138,7 +138,7 @@ End Test6_2.
 
 Module Test7.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Numeral.uint }.
+  Record wuint := wrap { unwrap : Number.uint }.
   Declare Scope wuint_scope.
   Delimit Scope wuint_scope with wuint.
   Number Notation wuint wrap unwrap : wuint_scope.
@@ -148,7 +148,7 @@ End Test7.
 
 Module Test8.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Numeral.uint }.
+  Record wuint := wrap { unwrap : Number.uint }.
   Declare Scope wuint8_scope.
   Declare Scope wuint8'_scope.
   Delimit Scope wuint8_scope with wuint8.
@@ -177,7 +177,7 @@ Module Test9.
   Delimit Scope wuint9'_scope with wuint9'.
   Section with_let.
     Local Set Primitive Projections.
-    Record wuint := wrap { unwrap : Numeral.uint }.
+    Record wuint := wrap { unwrap : Number.uint }.
     Let wrap' := wrap.
     Let unwrap' := unwrap.
     Local Notation wrap'' := wrap.
@@ -194,8 +194,8 @@ End Test9.
 Module Test10.
   (* Test that it is only a warning to add abstract after to an optional parsing function *)
   Definition to_uint (v : unit) := Nat.to_num_uint 0.
-  Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end.
-  Definition of_any_uint (v : Numeral.uint) := tt.
+  Definition of_uint (v : Number.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Number.uint) := tt.
   Declare Scope unit_scope.
   Declare Scope unit2_scope.
   Delimit Scope unit_scope with unit.
@@ -209,11 +209,11 @@ Module Test10.
 End Test10.
 
 Module Test12.
-  (* Test for numeral notations on context variables *)
+  (* Test for number notations on context variables *)
   Declare Scope test12_scope.
   Delimit Scope test12_scope with test12.
   Section test12.
-    Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit).
+    Context (to_uint : unit -> Number.uint) (of_uint : Number.uint -> unit).
 
     Number Notation unit of_uint to_uint : test12_scope.
     Check let v := 1%test12 in v : unit.
@@ -221,15 +221,15 @@ Module Test12.
 End Test12.
 
 Module Test13.
-  (* Test for numeral notations on notations which do not denote references *)
+  (* Test for number notations on notations which do not denote references *)
   Declare Scope test13_scope.
   Declare Scope test13'_scope.
   Declare Scope test13''_scope.
   Delimit Scope test13_scope with test13.
   Delimit Scope test13'_scope with test13'.
   Delimit Scope test13''_scope with test13''.
-  Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O.
-  Definition of_uint (x : Numeral.uint) : unit := tt.
+  Definition to_uint (x y : unit) : Number.uint := Nat.to_num_uint O.
+  Definition of_uint (x : Number.uint) : unit := tt.
   Definition to_uint_good := to_uint tt.
   Notation to_uint' := (to_uint tt).
   Notation to_uint'' := (to_uint _).
@@ -242,7 +242,7 @@ Module Test13.
 End Test13.
 
 Module Test14.
-  (* Test that numeral notations follow [Import], not [Require], and
+  (* Test that number notations follow [Import], not [Require], and
      also test that [Local Number Notation]s do not escape modules
      nor sections. *)
   Declare Scope test14_scope.
@@ -254,8 +254,8 @@ Module Test14.
   Delimit Scope test14''_scope with test14''.
   Delimit Scope test14'''_scope with test14'''.
   Module Inner.
-    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Local Number Notation unit of_uint to_uint : test14_scope.
     Global Number Notation unit of_uint to_uint : test14'_scope.
     Check let v := 0%test14 in v : unit.
@@ -267,8 +267,8 @@ Module Test14.
   Fail Check let v := 0%test14 in v : unit.
   Check let v := 0%test14' in v : unit.
   Section InnerSection.
-    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Local Number Notation unit of_uint to_uint : test14''_scope.
     Fail Global Number Notation unit of_uint to_uint : test14'''_scope.
     Check let v := 0%test14'' in v : unit.
@@ -283,8 +283,8 @@ Module Test15.
   Declare Scope test15_scope.
   Delimit Scope test15_scope with test15.
   Module Inner.
-    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Number Notation unit of_uint to_uint : test15_scope.
     Check let v := 0%test15 in v : unit.
   End Inner.
@@ -306,8 +306,8 @@ Module Test16.
   End A.
   Module F (a : A).
     Inductive Foo := foo (_ : a.T).
-    Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : Foo := foo a.t.
+    Definition to_uint (x : Foo) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : Foo := foo a.t.
     Global Number Notation Foo of_uint to_uint : test16_scope.
     Check let v := 0%test16 in v : Foo.
   End F.
@@ -352,8 +352,8 @@ Module Test18.
   Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}.
   Definition nat_of_Q (x : Q) : option nat
     := if Nat.eqb x.(den) 1 then Some (x.(num)) else None.
-  Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x).
-  Definition uint_of_Q (x : Q) : option Numeral.uint
+  Definition Q_of_uint (x : Number.uint) : Q := Q_of_nat (Nat.of_num_uint x).
+  Definition uint_of_Q (x : Q) : option Number.uint
     := option_map Nat.to_num_uint (nat_of_Q x).
 
   Number Notation Q Q_of_uint uint_of_Q : Q_scope.
@@ -411,7 +411,7 @@ Module Test20.
 
   Record > ty := { t : Type ; kt : known_type t }.
 
-  Definition ty_of_uint (x : Numeral.uint) : option ty
+  Definition ty_of_uint (x : Number.uint) : option ty
     := match Nat.of_num_uint x with
        | 0 => @Some ty zero
        | 1 => @Some ty one
@@ -421,7 +421,7 @@ Module Test20.
        | 5 => @Some ty type
        | _ => None
        end.
-  Definition uint_of_ty (x : ty) : Numeral.uint
+  Definition uint_of_ty (x : ty) : Number.uint
     := Nat.to_num_uint match kt x with
                    | prop => 3
                    | set => 4
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 09feca71e7..914e7f88c6 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -30,15 +30,15 @@ implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
+Number.number_beq: Number.number -> Number.number -> bool
 Nat.eqb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
-Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Number.uint_beq: Number.uint -> Number.uint -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
-Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Number.int_beq: Number.int -> Number.int -> bool
 Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
@@ -64,34 +64,34 @@ eq_true_rec:
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_sind:
   forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
 Hexadecimal.internal_int_dec_lb0:
   forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
-Numeral.internal_numeral_dec_lb:
-  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
 Decimal.internal_decimal_dec_lb:
   forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
 Hexadecimal.internal_int_dec_bl0:
   forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
-Numeral.internal_int_dec_lb1:
-  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
-Numeral.internal_int_dec_bl1:
-  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_bl:
   forall x y : Hexadecimal.hexadecimal,
   Hexadecimal.hexadecimal_beq x y = true -> x = y
-Numeral.internal_uint_dec_lb1:
-  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
 Decimal.internal_int_dec_bl:
   forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
 Decimal.internal_int_dec_lb:
   forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
-Numeral.internal_numeral_dec_bl:
-  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
@@ -160,21 +160,21 @@ f_equal2_mult:
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-Numeral.internal_numeral_dec_lb:
-  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
-Numeral.internal_int_dec_lb1:
-  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
-Numeral.internal_numeral_dec_bl:
-  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
-Numeral.internal_int_dec_bl1:
-  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
-Numeral.internal_uint_dec_lb1:
-  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Decimal.internal_decimal_dec_lb:
   forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
 Hexadecimal.internal_hexadecimal_dec_bl:
@@ -213,18 +213,18 @@ bool_choice:
   forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-Numeral.internal_numeral_dec_lb:
-  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
-Numeral.internal_numeral_dec_bl:
-  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
-Numeral.internal_int_dec_lb1:
-  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
-Numeral.internal_int_dec_bl1:
-  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
-Numeral.internal_uint_dec_lb1:
-  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
@@ -306,12 +306,12 @@ nat_rect_plus:
     (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) 
     (fun _ : nat => f) n
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Numeral.internal_numeral_dec_bl:
-  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
-Numeral.internal_int_dec_bl1:
-  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_bl:
   forall x y : Hexadecimal.hexadecimal,
   Hexadecimal.hexadecimal_beq x y = true -> x = y
@@ -328,12 +328,12 @@ Byte.to_bits_of_bits:
   forall
     b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
   Byte.to_bits (Byte.of_bits b) = b
-Numeral.internal_numeral_dec_lb:
-  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
-Numeral.internal_uint_dec_lb1:
-  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
-Numeral.internal_int_dec_lb1:
-  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
 Decimal.internal_int_dec_lb:
   forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
 Hexadecimal.internal_hexadecimal_dec_lb:
@@ -391,7 +391,7 @@ Nat.lor: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
 Nat.of_hex_uint: Hexadecimal.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
-Nat.of_num_uint: Numeral.uint -> nat
+Nat.of_num_uint: Number.uint -> nat
 length: forall [A : Type], list A -> nat
 plus_n_O: forall n : nat, n = n + 0
 plus_O_n: forall n : nat, 0 + n = n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 9554581ebe..2f0d854ac6 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -21,15 +21,15 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
-Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Number.uint_beq: Number.uint -> Number.uint -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
-Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
-Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Number.number_beq: Number.number -> Number.number -> bool
+Number.int_beq: Number.int -> Number.int -> bool
 Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
 Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 80b03e8a0b..d705ec898b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -7,15 +7,15 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
-Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Number.uint_beq: Number.uint -> Number.uint -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
-Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
-Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Number.number_beq: Number.number -> Number.number -> bool
+Number.int_beq: Number.int -> Number.int -> bool
 Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
 Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
@@ -50,7 +50,7 @@ Nat.lor: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
 Hexadecimal.nb_digits: Hexadecimal.uint -> nat
 Nat.of_hex_uint: Hexadecimal.uint -> nat
-Nat.of_num_uint: Numeral.uint -> nat
+Nat.of_num_uint: Number.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
 Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index 7b2bb00ce0..219d953c97 100644
--- a/test-suite/output/ZSyntax.v
+++ b/test-suite/output/ZSyntax.v
@@ -18,7 +18,7 @@ Require Import Arith.
 Check (0 + Z.of_nat 11)%Z.
 
 (* Check hexadecimal printing *)
-Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n).
+Definition to_num_int n := Number.IntHex (Z.to_hex_int n).
 Number Notation Z Z.of_num_int to_num_int : Z_scope.
 Check 42%Z.
 Check (-42)%Z.
diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
index 437b4a68e9..a7366f2d35 100644
--- a/test-suite/output/bug_12159.v
+++ b/test-suite/output/bug_12159.v
@@ -2,10 +2,10 @@ Declare Scope A.
 Declare Scope B.
 Delimit Scope A with A.
 Delimit Scope B with B.
-Definition to_unit (v : Numeral.uint) : option unit
+Definition to_unit (v : Number.uint) : option unit
   := match Nat.of_num_uint v with O => Some tt | _ => None end.
-Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
-Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1.
+Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
+Definition of_unit' (v : unit) : Number.uint := Nat.to_num_uint 1.
 Number Notation unit to_unit of_unit : A.
 Number Notation unit to_unit of_unit' : B.
 Definition f x : unit := x.
diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumberNotationsNoLocal.v
index fe97f10ddf..e19d06cfa7 100644
--- a/test-suite/success/NumeralNotationsNoLocal.v
+++ b/test-suite/success/NumberNotationsNoLocal.v
@@ -1,4 +1,4 @@
-(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+(* Test that number notations don't work on proof-local variables, especially not ones containing evars *)
 Inductive unit11 := tt11.
 Declare Scope unit11_scope.
 Delimit Scope unit11_scope with unit11.