Rename Dec and HexDec to Decimal and Hexadecimal

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

3 files changed, 5 insertions, 5 deletions

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.