Merge PR #12979: Uniformize names for number literals between parsing and refman

Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: Zimmi48
Ack-by: proux01

13 files changed, 26 insertions, 26 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 5eae5567d7..025264ab01 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -12,7 +12,7 @@
 
 (** These numbers coded in base 10 will be used for parsing and printing
     other Coq numeral datatypes in an human-readable way.
-    See the [Numeral Notation] command.
+    See the [Number Notation] command.
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
@@ -245,7 +245,7 @@ with succ_double d :=
 End Little.
 
 (** Pseudo-conversion functions used when declaring
-    Numeral Notations on [uint] and [int]. *)
+    Number Notations on [uint] and [int]. *)
 
 Definition uint_of_uint (i:uint) := i.
 Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v
index a4ddad2875..36f5e5ad1f 100644
--- a/theories/Init/Hexadecimal.v
+++ b/theories/Init/Hexadecimal.v
@@ -12,7 +12,7 @@
 
 (** These numbers coded in base 16 will be used for parsing and printing
     other Coq numeral datatypes in an human-readable way.
-    See the [Numeral Notation] command.
+    See the [Number Notation] command.
     We represent numbers in base 16 as lists of hexadecimal digits,
     in big-endian order (most significant digit comes first). *)
 
diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v
index 8a0531e004..179547d0b3 100644
--- a/theories/Init/Numeral.v
+++ b/theories/Init/Numeral.v
@@ -27,7 +27,7 @@ Register int as num.num_int.type.
 Register numeral as num.numeral.type.
 
 (** Pseudo-conversion functions used when declaring
-    Numeral Notations on [uint] and [int]. *)
+    Number Notations on [uint] and [int]. *)
 
 Definition uint_of_uint (i:uint) := i.
 Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 8f862e8cec..0fe3d5491e 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -35,22 +35,22 @@ Declare ML Module "string_notation_plugin".
 (* Parsing / printing of hexadecimal numbers *)
 Arguments Nat.of_hex_uint d%hex_uint_scope.
 Arguments Nat.of_hex_int d%hex_int_scope.
-Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
   : hex_uint_scope.
-Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
   : hex_int_scope.
 
 (* Parsing / printing of decimal numbers *)
 Arguments Nat.of_uint d%dec_uint_scope.
 Arguments Nat.of_int d%dec_int_scope.
-Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
   : dec_uint_scope.
-Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
   : dec_int_scope.
 
 (* Parsing / printing of [nat] numbers *)
-Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001).
-Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001).
+Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001).
+Number Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001).
 
 (* Printing/Parsing of bytes *)
 Export Byte.ByteSyntaxNotations.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 1881e387a2..28ba9daed0 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -1007,7 +1007,7 @@ Bind Scope N_scope with N.t N.
 
 (** Exportation of notations *)
 
-Numeral Notation N N.of_num_uint N.to_num_uint : N_scope.
+Number Notation N N.of_num_uint N.to_num_uint : N_scope.
 
 Infix "+" := N.add : N_scope.
 Infix "-" := N.sub : N_scope.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 8a0aee9cf4..222e76c3e7 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -434,9 +434,9 @@ Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n).
 
 Definition to_num_int n := Numeral.IntDec (to_int n).
 
-Numeral Notation N of_num_uint to_num_uint : N_scope.
+Number Notation N of_num_uint to_num_uint : N_scope.
 
 End N.
 
 (** Re-export the notation for those who just [Import NatIntDef] *)
-Numeral Notation N N.of_num_uint N.to_num_uint : N_scope.
+Number Notation N N.of_num_uint N.to_num_uint : N_scope.
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 5585f478b3..7c846571a7 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -8,12 +8,12 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** * Alternative Binary Numeral Notations *)
+(** * Alternative Binary Number Notations *)
 
 (** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
 
 (** By default, literals in types [positive], [N], [Z] are parsed and
-    printed via the [Numeral Notation] command, by conversion from/to
+    printed via the [Number Notation] command, by conversion from/to
     the [Decimal.int] representation. When working with numbers with
     thousands of digits and more, conversion from/to [Decimal.int] can
     become significantly slow. If that becomes a problem for your
@@ -43,7 +43,7 @@ Definition pos_of_z z :=
 
 Definition pos_to_z p := Zpos p.
 
-Numeral Notation positive pos_of_z pos_to_z : positive_scope.
+Number Notation positive pos_of_z pos_to_z : positive_scope.
 
 (** [N] *)
 
@@ -60,10 +60,10 @@ Definition n_to_z n :=
     | Npos p => Zpos p
   end.
 
-Numeral Notation N n_of_z n_to_z : N_scope.
+Number Notation N n_of_z n_to_z : N_scope.
 
 (** [Z] *)
 
 Definition z_of_z (z:Z) := z.
 
-Numeral Notation Z z_of_z z_of_z : Z_scope.
+Number Notation Z z_of_z z_of_z : Z_scope.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index cd814091a1..d3528ce87c 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -477,4 +477,4 @@ Definition tail031 (i:int31) :=
     end)
    i On.
 
-Numeral Notation int31 phi_inv_nonneg phi : int31_scope.
+Number Notation int31 phi_inv_nonneg phi : int31_scope.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index c8414c241d..e73060af0b 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1886,7 +1886,7 @@ Bind Scope positive_scope with Pos.t positive.
 
 (** Exportation of notations *)
 
-Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope.
+Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope.
 
 Infix "+" := Pos.add : positive_scope.
 Infix "-" := Pos.sub : positive_scope.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index cdb9af542c..b41cd571dc 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -697,9 +697,9 @@ Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p).
 
 Definition to_num_int n := Numeral.IntDec (to_int n).
 
-Numeral Notation positive of_num_int to_num_uint : positive_scope.
+Number Notation positive of_num_int to_num_uint : positive_scope.
 
 End Pos.
 
 (** Re-export the notation for those who just [Import BinPosDef] *)
-Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope.
+Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 84d70e56de..192dcd885b 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -129,7 +129,7 @@ Definition to_numeral (q:Q) : option Numeral.numeral :=
   | Some q => Some (Numeral.Dec q)
   end.
 
-Numeral Notation Q of_numeral to_numeral : Q_scope.
+Number Notation Q of_numeral to_numeral : Q_scope.
 
 Definition inject_Z (x : Z) := Qmake x 1.
 Arguments inject_Z x%Z.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a566348dd5..9a30e011af 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1297,7 +1297,7 @@ Bind Scope Z_scope with Z.t Z.
 
 (** Re-export Notations *)
 
-Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope.
+Number Notation Z Z.of_num_int Z.to_num_int : Z_scope.
 
 Infix "+" := Z.add : Z_scope.
 Notation "- x" := (Z.opp x) : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 8464ad1012..69ed101f24 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -668,9 +668,9 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
-Numeral Notation Z of_num_int to_num_int : Z_scope.
+Number Notation Z of_num_int to_num_int : Z_scope.
 
 End Z.
 
 (** Re-export the notation for those who just [Import BinIntDef] *)
-Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope.
+Number Notation Z Z.of_num_int Z.to_num_int : Z_scope.