Rename Dec and HexDec to Decimal and Hexadecimal

As noted by Hugo Herbelin, Dec is rather used for "decidable".

13 files changed, 72 insertions, 60 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2af40792df..9d1fcc160d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1884,7 +1884,7 @@ The following errors apply to both string and number notations:
           | _ => None end in
         f (Decimal.rev u).
       Definition of_uint (u : Number.uint) : option radix3 :=
-        match u with Number.UIntDec u => of_uint_dec u | Number.UIntHex _ => None end.
+        match u with Number.UIntDecimal u => of_uint_dec u | Number.UIntHexadecimal _ => None end.
 
    and a printing function
 
@@ -1897,7 +1897,7 @@ The following errors apply to both string and number notations:
           | x3p1 x => Decimal.D1 (f x)
           | x3p2 x => Decimal.D2 (f x) end in
         Decimal.rev (f x).
-      Definition to_uint (x : radix3) : Number.uint := Number.UIntDec (to_uint_dec x).
+      Definition to_uint (x : radix3) : Number.uint := Number.UIntDecimal (to_uint_dec x).
 
    before declaring the notation
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 10e620b58a..a0321aaf82 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -836,8 +836,8 @@ let coqnumber_of_rawnum inds c n =
     mkApp (mkConstruct (ind, 2), [|i; f; e|])  (* (D|Hexad)ecimalExp *)
 
 let mkDecHex ind c n = match c with
-  | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Dec *)
-  | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hex *)
+  | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Decimal *)
+  | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hexadecimal *)
 
 exception NonDecimal
 
@@ -912,8 +912,8 @@ let rawnum_of_coqnumber cl c =
 let destDecHex c = match Constr.kind c with
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c'
-      | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c'
+      | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c'
+      | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c'
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 57206772c8..60682edec8 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -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 (Number.UIntDec (Decimal.D1 Decimal.Nil)) : punit
+v := pto_punits (Number.UIntDecimal (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 := Number.UIntDec (Decimal.D0 Decimal.Nil) |}
+     = {| unwrap := Number.UIntDecimal (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 (Number.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit
+let v := of_uint (Number.UIntDecimal (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 556cf929b4..718da13500 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -569,7 +569,7 @@ Inductive I' :=
 | I'unit : I'
 | I'sum : I -> I' -> I'.
 Definition of_uint' (x : Number.uint) : I' := I'empty.
-Definition to_uint' (x : I') : Number.uint := Number.UIntDec Decimal.Nil.
+Definition to_uint' (x : I') : Number.uint := Number.UIntDecimal Decimal.Nil.
 Number Notation nSet of_uint' to_uint' (via I'
   mapping [Empty_set => I'empty, unit => I'unit, sum => I'sum])
   : type_scope.
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index 219d953c97..67c4f85d5c 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 := Number.IntHex (Z.to_hex_int n).
+Definition to_num_int n := Number.IntHexadecimal (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/theories/Init/Nat.v b/theories/Init/Nat.v
index bc48311151..9a3a3ec99b 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -214,8 +214,8 @@ Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
 
 Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Number.UIntDec d => of_uint d
-  | Number.UIntHex d => of_hex_uint d
+  | Number.UIntDecimal d => of_uint d
+  | Number.UIntHexadecimal 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 := Number.UIntDec (to_uint n).
+Definition to_num_uint n := Number.UIntDecimal (to_uint n).
 
-Definition to_num_hex_uint n := Number.UIntHex (to_hex_uint n).
+Definition to_num_hex_uint n := Number.UIntHexadecimal (to_hex_uint n).
 
 Definition of_int (d:Decimal.int) : option nat :=
   match Decimal.norm d with
@@ -254,15 +254,15 @@ Definition of_hex_int (d:Hexadecimal.int) : option nat :=
 
 Definition of_num_int (d:Number.int) : option nat :=
   match d with
-  | Number.IntDec d => of_int d
-  | Number.IntHex d => of_hex_int d
+  | Number.IntDecimal d => of_int d
+  | Number.IntHexadecimal 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 := Number.IntDec (to_int n).
+Definition to_num_int n := Number.IntDecimal (to_int n).
 
 (** ** Euclidean division *)
 
diff --git a/theories/Init/Number.v b/theories/Init/Number.v
index 228f84b179..eb9cc856ac 100644
--- a/theories/Init/Number.v
+++ b/theories/Init/Number.v
@@ -12,11 +12,23 @@
 
 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).
+Variant uint := UIntDecimal (u:Decimal.uint) | UIntHexadecimal (u:Hexadecimal.uint).
+#[deprecated(since="8.13",note="Use UintDecimal instead.")]
+Notation UIntDec := UIntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use UintHexadecimal instead.")]
+Notation UIntHex := UIntHexadecimal (only parsing).
+
+Variant int := IntDecimal (i:Decimal.int) | IntHexadecimal (i:Hexadecimal.int).
+#[deprecated(since="8.13",note="Use IntDecimal instead.")]
+Notation IntDec := IntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use IntHexadecimal instead.")]
+Notation IntHex := IntHexadecimal (only parsing).
+
+Variant number := Decimal (d:Decimal.decimal) | Hexadecimal (h:Hexadecimal.hexadecimal).
+#[deprecated(since="8.13",note="Use Decimal instead.")]
+Notation Dec := Decimal (only parsing).
+#[deprecated(since="8.13",note="Use Hexadecimal instead.")]
+Notation Hex := Hexadecimal (only parsing).
 
 Scheme Equality for uint.
 Scheme Equality for int.
diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v
index c87f17ee5a..50fa312e7e 100644
--- a/theories/Init/Numeral.v
+++ b/theories/Init/Numeral.v
@@ -14,24 +14,24 @@ 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.UintDecimal instead.")]
+Notation UIntDec := UIntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintHexadecimal instead.")]
+Notation UIntHex := UIntHexadecimal (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.IntDecimal instead.")]
+Notation IntDec := IntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntHexadecimal instead.")]
+Notation IntHex := IntHexadecimal (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.Decimal instead.")]
+Notation Dec := Decimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.Hexadecimal instead.")]
+Notation Hex := Hexadecimal (only parsing).
 
 #[deprecated(since="8.13",note="Use Number.uint_beq instead.")]
 Notation uint_beq := uint_beq (only parsing).
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 4142bb786f..e57e5fe856 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -392,8 +392,8 @@ Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d.
 
 Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Number.UIntDec d => of_uint d
-  | Number.UIntHex d => of_hex_uint d
+  | Number.UIntDecimal d => of_uint d
+  | Number.UIntHexadecimal d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) :=
@@ -410,8 +410,8 @@ Definition of_hex_int (d:Hexadecimal.int) :=
 
 Definition of_num_int (d:Number.int) :=
   match d with
-  | Number.IntDec d => of_int d
-  | Number.IntHex d => of_hex_int d
+  | Number.IntDecimal d => of_int d
+  | Number.IntHexadecimal 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 := Number.UIntDec (to_uint n).
+Definition to_num_uint n := Number.UIntDecimal (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 := Number.IntDec (to_int n).
+Definition to_num_int n := Number.IntDecimal (to_int n).
 
 Number Notation N of_num_uint to_num_uint : N_scope.
 
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 958778762d..2ec9f4d871 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -641,8 +641,8 @@ Fixpoint of_hex_uint (d:Hexadecimal.uint) : N :=
 
 Definition of_num_uint (d:Number.uint) : N :=
   match d with
-  | Number.UIntDec d => of_uint d
-  | Number.UIntHex d => of_hex_uint d
+  | Number.UIntDecimal d => of_uint d
+  | Number.UIntHexadecimal d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) : option positive :=
@@ -667,8 +667,8 @@ Definition of_hex_int (d:Hexadecimal.int) : option positive :=
 
 Definition of_num_int (d:Number.int) : option positive :=
   match d with
-  | Number.IntDec d => of_int d
-  | Number.IntHex d => of_hex_int d
+  | Number.IntDecimal d => of_int d
+  | Number.IntHexadecimal 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 := Number.UIntDec (to_uint p).
+Definition to_num_uint p := Number.UIntDecimal (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 := Number.IntDec (to_int n).
+Definition to_num_int n := Number.IntDecimal (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 9a70ac311a..fa4f9134cc 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -396,20 +396,20 @@ Definition to_hexadecimal (n : IQ) : option Hexadecimal.hexadecimal :=
 
 Definition of_number (n : Number.number) : IQ :=
   match n with
-  | Number.Dec d => of_decimal d
-  | Number.Hex h => of_hexadecimal h
+  | Number.Decimal d => of_decimal d
+  | Number.Hexadecimal h => of_hexadecimal h
   end.
 
 Definition to_number (q:IQ) : option Number.number :=
   match to_decimal q with
   | None => None
-  | Some q => Some (Number.Dec q)
+  | Some q => Some (Number.Decimal q)
   end.
 
 Definition to_hex_number q :=
   match to_hexadecimal q with
   | None => None
-  | Some q => Some (Number.Hex q)
+  | Some q => Some (Number.Hexadecimal q)
   end.
 
 Number Notation Q of_number to_hex_number (via IQ
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index ac82216474..40736c61f2 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -280,8 +280,8 @@ Definition of_hexadecimal (d : Hexadecimal.hexadecimal) : IR :=
 
 Definition of_number (n : Number.number) : IR :=
   match n with
-  | Number.Dec d => of_decimal d
-  | Number.Hex h => of_hexadecimal h
+  | Number.Decimal d => of_decimal d
+  | Number.Hexadecimal h => of_hexadecimal h
   end.
 
 Definition IQmake_to_decimal num den :=
@@ -369,13 +369,13 @@ Definition to_hexadecimal (n : IR) : option Hexadecimal.hexadecimal :=
 Definition to_number q :=
   match to_decimal q with
   | None => None
-  | Some q => Some (Number.Dec q)
+  | Some q => Some (Number.Decimal q)
   end.
 
 Definition to_hex_number q :=
   match to_hexadecimal q with
   | None => None
-  | Some q => Some (Number.Hex q)
+  | Some q => Some (Number.Hexadecimal q)
   end.
 
 Number Notation R of_number to_hex_number (via IR
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 9415903fa4..58bc75b62c 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -313,8 +313,8 @@ Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d).
 
 Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Number.UIntDec d => of_uint d
-  | Number.UIntHex d => of_hex_uint d
+  | Number.UIntDecimal d => of_uint d
+  | Number.UIntHexadecimal d => of_hex_uint d
   end.
 
 Definition of_int (d:Decimal.int) :=
@@ -331,8 +331,8 @@ Definition of_hex_int (d:Hexadecimal.int) :=
 
 Definition of_num_int (d:Number.int) :=
   match d with
-  | Number.IntDec d => of_int d
-  | Number.IntHex d => of_hex_int d
+  | Number.IntDecimal d => of_int d
+  | Number.IntHexadecimal 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 := Number.IntDec (to_int n).
+Definition to_num_int n := Number.IntDecimal (to_int n).
 
 (** ** Iteration of a function