Renaming Numeral.v into Number.v

9 files changed, 121 insertions, 66 deletions

diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 7c8cf0b536..bc48311151 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import Notations Logic Datatypes.
-Require Decimal Hexadecimal Numeral.
+Require Decimal Hexadecimal Number.
 Local Open Scope nat_scope.
 
 (**********************************************************************)
@@ -212,10 +212,10 @@ Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
 
 Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
 
-Definition of_num_uint (d:Numeral.uint) :=
+Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Numeral.UIntDec d => of_uint d
-  | Numeral.UIntHex d => of_hex_uint d
+  | Number.UIntDec d => of_uint d
+  | Number.UIntHex d => of_hex_uint d
   end.
 
 Fixpoint to_little_uint n acc :=
@@ -236,9 +236,9 @@ Fixpoint to_little_hex_uint n acc :=
 Definition to_hex_uint n :=
   Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero).
 
-Definition to_num_uint n := Numeral.UIntDec (to_uint n).
+Definition to_num_uint n := Number.UIntDec (to_uint n).
 
-Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n).
+Definition to_num_hex_uint n := Number.UIntHex (to_hex_uint n).
 
 Definition of_int (d:Decimal.int) : option nat :=
   match Decimal.norm d with
@@ -252,17 +252,17 @@ Definition of_hex_int (d:Hexadecimal.int) : option nat :=
     | _ => None
   end.
 
-Definition of_num_int (d:Numeral.int) : option nat :=
+Definition of_num_int (d:Number.int) : option nat :=
   match d with
-  | Numeral.IntDec d => of_int d
-  | Numeral.IntHex d => of_hex_int d
+  | Number.IntDec d => of_int d
+  | Number.IntHex d => of_hex_int d
   end.
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
 Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n).
 
-Definition to_num_int n := Numeral.IntDec (to_int n).
+Definition to_num_int n := Number.IntDec (to_int n).
 
 (** ** Euclidean division *)
 
diff --git a/theories/Init/Number.v b/theories/Init/Number.v
new file mode 100644
index 0000000000..228f84b179
--- /dev/null
+++ b/theories/Init/Number.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Decimal or Hexadecimal numbers *)
+
+Require Import Decimal Hexadecimal.
+
+Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).
+
+Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int).
+
+Variant number := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).
+
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for number.
+
+Register uint as num.num_uint.type.
+Register int as num.num_int.type.
+Register number as num.number.type.
+
+(** Pseudo-conversion functions used when declaring
+    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/Numeral.v b/theories/Init/Numeral.v
index 179547d0b3..c87f17ee5a 100644
--- a/theories/Init/Numeral.v
+++ b/theories/Init/Numeral.v
@@ -8,26 +8,47 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** * Decimal or Hexadecimal numbers *)
-
-Require Import Decimal Hexadecimal.
-
-Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).
-
-Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int).
-
-Variant numeral := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).
-
-Scheme Equality for uint.
-Scheme Equality for int.
-Scheme Equality for numeral.
-
-Register uint as num.num_uint.type.
-Register int as num.num_int.type.
-Register numeral as num.numeral.type.
-
-(** Pseudo-conversion functions used when declaring
-    Number Notations on [uint] and [int]. *)
-
-Definition uint_of_uint (i:uint) := i.
-Definition int_of_int (i:int) := i.
+(** * Deprecated: use Number.v instead *)
+
+Require Import Decimal Hexadecimal Number.
+
+#[deprecated(since="8.13",note="Use Number.uint instead.")]
+Notation uint := uint (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintDec instead.")]
+Notation UIntDec := UIntDec (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintHex instead.")]
+Notation UIntHex := UIntHex (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.int instead.")]
+Notation int := int (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntDec instead.")]
+Notation IntDec := IntDec (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntHex instead.")]
+Notation IntHex := IntHex (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.numeral instead.")]
+Notation numeral := number (only parsing).
+#[deprecated(since="8.13",note="Use Number.Dec instead.")]
+Notation Dec := Dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.Hex instead.")]
+Notation Hex := Hex (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.uint_beq instead.")]
+Notation uint_beq := uint_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.uint_eq_dec instead.")]
+Notation uint_eq_dec := uint_eq_dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_beq instead.")]
+Notation int_beq := int_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_eq_dec instead.")]
+Notation int_eq_dec := int_eq_dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.numeral_beq instead.")]
+Notation numeral_beq := number_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.numeral_eq_dec instead.")]
+Notation numeral_eq_dec := number_eq_dec (only parsing).
+
+Register number as num.numeral.type.
+
+#[deprecated(since="8.13",note="Use Number.uint_of_uint instead.")]
+Notation uint_of_uint := uint_of_uint (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_of_int instead.")]
+Notation int_of_int := int_of_int (only parsing).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 0fe3d5491e..141864d257 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -17,6 +17,7 @@ Require Coq.Init.Byte.
 Require Coq.Init.Decimal.
 Require Coq.Init.Hexadecimal.
 Require Coq.Init.Numeral.
+Require Coq.Init.Number.
 Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
@@ -35,17 +36,17 @@ 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.
-Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
   : hex_uint_scope.
-Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Number.int Number.int_of_int Number.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.
-Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
   : dec_uint_scope.
-Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Number.int Number.int_of_int Number.int_of_int
   : dec_int_scope.
 
 (* Parsing / printing of [nat] numbers *)
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 222e76c3e7..4142bb786f 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -390,10 +390,10 @@ Definition of_uint (d:Decimal.uint) := Pos.of_uint d.
 
 Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d.
 
-Definition of_num_uint (d:Numeral.uint) :=
+Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Numeral.UIntDec d => of_uint d
-  | Numeral.UIntHex d => of_hex_uint d
+  | Number.UIntDec d => of_uint d
+  | Number.UIntHex d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) :=
@@ -408,10 +408,10 @@ Definition of_hex_int (d:Hexadecimal.int) :=
   | Hexadecimal.Neg _ => None
   end.
 
-Definition of_num_int (d:Numeral.int) :=
+Definition of_num_int (d:Number.int) :=
   match d with
-  | Numeral.IntDec d => of_int d
-  | Numeral.IntHex d => of_hex_int d
+  | Number.IntDec d => of_int d
+  | Number.IntHex d => of_hex_int d
   end.
 
 Definition to_uint n :=
@@ -426,13 +426,13 @@ Definition to_hex_uint n :=
   | pos p => Pos.to_hex_uint p
   end.
 
-Definition to_num_uint n := Numeral.UIntDec (to_uint n).
+Definition to_num_uint n := Number.UIntDec (to_uint n).
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
 Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n).
 
-Definition to_num_int n := Numeral.IntDec (to_int n).
+Definition to_num_int n := Number.IntDec (to_int n).
 
 Number Notation N of_num_uint to_num_uint : N_scope.
 
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 7c846571a7..c203c178f5 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -17,7 +17,7 @@
     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
-    development, this file provides some alternative [Numeral
+    development, this file provides some alternative [Number
     Notation] commands that use [Z] as bridge type. To enable these
     commands, just be sure to [Require] this file after other files
     defining numeral notations.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index b41cd571dc..958778762d 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -639,10 +639,10 @@ Fixpoint of_hex_uint (d:Hexadecimal.uint) : N :=
   | Hexadecimal.Df l => Npos (of_hex_uint_acc l 1~1~1~1)
   end.
 
-Definition of_num_uint (d:Numeral.uint) : N :=
+Definition of_num_uint (d:Number.uint) : N :=
   match d with
-  | Numeral.UIntDec d => of_uint d
-  | Numeral.UIntHex d => of_hex_uint d
+  | Number.UIntDec d => of_uint d
+  | Number.UIntHex d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) : option positive :=
@@ -665,10 +665,10 @@ Definition of_hex_int (d:Hexadecimal.int) : option positive :=
   | Hexadecimal.Neg _ => None
   end.
 
-Definition of_num_int (d:Numeral.int) : option positive :=
+Definition of_num_int (d:Number.int) : option positive :=
   match d with
-  | Numeral.IntDec d => of_int d
-  | Numeral.IntHex d => of_hex_int d
+  | Number.IntDec d => of_int d
+  | Number.IntHex d => of_hex_int d
   end.
 
 Fixpoint to_little_uint p :=
@@ -689,13 +689,13 @@ Fixpoint to_little_hex_uint p :=
 
 Definition to_hex_uint p := Hexadecimal.rev (to_little_hex_uint p).
 
-Definition to_num_uint p := Numeral.UIntDec (to_uint p).
+Definition to_num_uint p := Number.UIntDec (to_uint p).
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
 Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p).
 
-Definition to_num_int n := Numeral.IntDec (to_int n).
+Definition to_num_int n := Number.IntDec (to_int n).
 
 Number Notation positive of_num_int to_num_uint : positive_scope.
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 192dcd885b..151355519e 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -117,16 +117,16 @@ Definition to_hexadecimal (q:Q) : option Hexadecimal.hexadecimal :=
   | _ => None
   end.
 
-Definition of_numeral (d:Numeral.numeral) : option Q :=
+Definition of_numeral (d:Number.number) : option Q :=
   match d with
-  | Numeral.Dec d => Some (of_decimal d)
-  | Numeral.Hex d => Some (of_hexadecimal d)
+  | Number.Dec d => Some (of_decimal d)
+  | Number.Hex d => Some (of_hexadecimal d)
   end.
 
-Definition to_numeral (q:Q) : option Numeral.numeral :=
+Definition to_numeral (q:Q) : option Number.number :=
   match to_decimal q with
   | None => None
-  | Some q => Some (Numeral.Dec q)
+  | Some q => Some (Number.Dec q)
   end.
 
 Number Notation Q of_numeral to_numeral : Q_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 69ed101f24..9415903fa4 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -311,10 +311,10 @@ Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d).
 
 Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d).
 
-Definition of_num_uint (d:Numeral.uint) :=
+Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Numeral.UIntDec d => of_uint d
-  | Numeral.UIntHex d => of_hex_uint d
+  | Number.UIntDec d => of_uint d
+  | Number.UIntHex d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) :=
@@ -329,10 +329,10 @@ Definition of_hex_int (d:Hexadecimal.int) :=
   | Hexadecimal.Neg d => opp (of_hex_uint d)
   end.
 
-Definition of_num_int (d:Numeral.int) :=
+Definition of_num_int (d:Number.int) :=
   match d with
-  | Numeral.IntDec d => of_int d
-  | Numeral.IntHex d => of_hex_int d
+  | Number.IntDec d => of_int d
+  | Number.IntHex d => of_hex_int d
   end.
 
 Definition to_int n :=
@@ -349,7 +349,7 @@ Definition to_hex_int n :=
   | neg p => Hexadecimal.Neg (Pos.to_hex_uint p)
   end.
 
-Definition to_num_int n := Numeral.IntDec (to_int n).
+Definition to_num_int n := Number.IntDec (to_int n).
 
 (** ** Iteration of a function