Renaming Numeral.v into Number.v

4 files changed, 92 insertions, 37 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 *)