Merge PR #11948: Hexadecimal numerals

Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin

18 files changed, 450 insertions, 113 deletions

diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 7941d2e647..4a5a700879 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -42,13 +42,25 @@ closest value will be used and unambiguously printed
      : float
 2.5 + 2.5
      : float
-File "stdin", line 24, characters 6-11:
+-26
+     : float
+11.171875
+     : float
+-6882
+     : float
+44.6875
+     : float
+2860
+     : float
+-2.79296875
+     : float
+File "stdin", line 30, characters 6-11:
 Warning: The constant 1e309 is not a binary64 floating-point value. A closest
 value will be used and unambiguously printed infinity.
 [inexact-float,parsing]
 infinity
      : float
-File "stdin", line 25, characters 6-12:
+File "stdin", line 31, characters 6-12:
 Warning: The constant -1e309 is not a binary64 floating-point value. A
 closest value will be used and unambiguously printed neg_infinity.
 [inexact-float,parsing]
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index eca712db10..36ffc27239 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -20,6 +20,12 @@ Check 2.5e123.
 Check (-2.5e-123).
 Check (2 + 2).
 Check (2.5 + 2.5).
+Check -0x1a.
+Check 0xb.2c.
+Check -0x1ae2.
+Check 0xb.2cp2.
+Check 0xb.2cp8.
+Check -0xb.2cp-2.
 
 Check 1e309.
 Check -1e309.
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index 4d76f1210b..eefa338f0d 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -6,6 +6,32 @@
      : int
 9223372036854775807
      : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+0
+     : int
+0
+     : int
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+The command has indeed failed with message:
+The reference x1 was not found in the current environment.
+The command has indeed failed with message:
+The reference x was not found in the current environment.
 2 + 2
      : int
 2 + 2
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 0385e529bf..c49616d918 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -5,6 +5,19 @@ Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap5.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP5.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
 Check (Int63.add 2 2).
 Check (2+2).
 Eval vm_compute in 2+2.
diff --git a/test-suite/output/NatSyntax.out b/test-suite/output/NatSyntax.out
new file mode 100644
index 0000000000..3067896d7a
--- /dev/null
+++ b/test-suite/output/NatSyntax.out
@@ -0,0 +1,34 @@
+42
+     : nat
+0
+     : nat
+0
+     : nat
+427
+     : nat
+427
+     : nat
+427
+     : nat
+427
+     : nat
+427
+     : nat
+The command has indeed failed with message:
+Cannot interpret this number as a value of type nat
+The command has indeed failed with message:
+Cannot interpret this number as a value of type nat
+0
+     : nat
+0
+     : nat
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+The command has indeed failed with message:
+The reference x1 was not found in the current environment.
+The command has indeed failed with message:
+The reference x was not found in the current environment.
+0x2a
+     : nat
diff --git a/test-suite/output/NatSyntax.v b/test-suite/output/NatSyntax.v
new file mode 100644
index 0000000000..66f697d412
--- /dev/null
+++ b/test-suite/output/NatSyntax.v
@@ -0,0 +1,18 @@
+Check 42.
+Check 0.
+Check 00.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap1.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP1.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
+Open Scope hex_nat_scope.
+Check 42.
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 060877707b..34c31ff8a6 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.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 (Decimal.D1 Decimal.Nil) : punit
+v := pto_punits (Numeral.UIntDec (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 := Decimal.D0 Decimal.Nil |}
+     = {| unwrap := Numeral.UIntDec (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 (Decimal.D1 Decimal.Nil) in v : unit
+let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit
      : unit
 let v := 0%test13 in v : unit
      : unit
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 47e1b127cb..ca8a14cce1 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -5,17 +5,17 @@ Declare Scope opaque_scope.
 (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
 Module Test1.
   Axiom hold : forall {A B C}, A -> B -> C.
-  Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
-  Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope.
+  Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
+  Numeral Notation Numeral.int opaque3 opaque3 : opaque_scope.
   Delimit Scope opaque_scope with opaque.
   Fail Check 1%opaque.
 End Test1.
 
 (* https://github.com/coq/coq/pull/8064#discussion_r202497990 *)
 Module Test2.
-  Axiom opaque4 : option Decimal.int.
-  Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4.
-  Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope.
+  Axiom opaque4 : option Numeral.int.
+  Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4.
+  Numeral Notation Numeral.int opaque6 opaque6 : opaque_scope.
   Delimit Scope opaque_scope with opaque.
   Open Scope opaque_scope.
   Fail Check 1%opaque.
@@ -24,8 +24,8 @@ End Test2.
 Declare Scope silly_scope.
 
 Module Test3.
-  Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A).
-  Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x).
+  Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A).
+  Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x).
   Definition of_silly (v : silly) := match v with SILLY v _ => v end.
   Numeral Notation silly to_silly of_silly : silly_scope.
   Delimit Scope silly_scope with silly.
@@ -45,15 +45,15 @@ Module Test4.
   Declare Scope upp.
   Declare Scope ppps.
   Polymorphic NonCumulative Inductive punit := ptt.
-  Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
-  Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt.
-  Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
-  Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
-  Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
-  Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
-  Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
-  Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
-  Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+  Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt.
+  Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0.
+  Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0.
+  Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
+  Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
   Numeral Notation punit to_punit of_punit : pto.
   Numeral Notation punit pto_punit of_punit : ppo.
   Numeral Notation punit to_punit pof_punit : ptp.
@@ -113,8 +113,8 @@ Module Test6.
 
   Local Set Primitive Projections.
   Record > wnat := wrap { unwrap :> nat }.
-  Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x.
-  Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x.
+  Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x.
+  Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x.
   Module Export Scopes.
     Declare Scope wnat_scope.
     Delimit Scope wnat_scope with wnat.
@@ -138,7 +138,7 @@ End Test6_2.
 
 Module Test7.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Decimal.uint }.
+  Record wuint := wrap { unwrap : Numeral.uint }.
   Declare Scope wuint_scope.
   Delimit Scope wuint_scope with wuint.
   Numeral Notation wuint wrap unwrap : wuint_scope.
@@ -148,7 +148,7 @@ End Test7.
 
 Module Test8.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Decimal.uint }.
+  Record wuint := wrap { unwrap : Numeral.uint }.
   Declare Scope wuint8_scope.
   Declare Scope wuint8'_scope.
   Delimit Scope wuint8_scope with wuint8.
@@ -162,7 +162,7 @@ Module Test8.
   End with_var.
   Check let v := 0%wuint8 in v : nat.
   Fail Check let v := 0%wuint8 in v : wuint.
-  Compute wrap (Nat.to_uint 0).
+  Compute wrap (Nat.to_num_uint 0).
 
   Notation wrap'' := wrap.
   Notation unwrap'' := unwrap.
@@ -177,7 +177,7 @@ Module Test9.
   Delimit Scope wuint9'_scope with wuint9'.
   Section with_let.
     Local Set Primitive Projections.
-    Record wuint := wrap { unwrap : Decimal.uint }.
+    Record wuint := wrap { unwrap : Numeral.uint }.
     Let wrap' := wrap.
     Let unwrap' := unwrap.
     Local Notation wrap'' := wrap.
@@ -193,9 +193,9 @@ End Test9.
 
 Module Test10.
   (* Test that it is only a warning to add abstract after to an optional parsing function *)
-  Definition to_uint (v : unit) := Nat.to_uint 0.
-  Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end.
-  Definition of_any_uint (v : Decimal.uint) := tt.
+  Definition to_uint (v : unit) := Nat.to_num_uint 0.
+  Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Numeral.uint) := tt.
   Declare Scope unit_scope.
   Declare Scope unit2_scope.
   Delimit Scope unit_scope with unit.
@@ -213,7 +213,7 @@ Module Test12.
   Declare Scope test12_scope.
   Delimit Scope test12_scope with test12.
   Section test12.
-    Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit).
+    Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit).
 
     Numeral Notation unit of_uint to_uint : test12_scope.
     Check let v := 1%test12 in v : unit.
@@ -228,8 +228,8 @@ Module Test13.
   Delimit Scope test13_scope with test13.
   Delimit Scope test13'_scope with test13'.
   Delimit Scope test13''_scope with test13''.
-  Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O.
-  Definition of_uint (x : Decimal.uint) : unit := tt.
+  Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O.
+  Definition of_uint (x : Numeral.uint) : unit := tt.
   Definition to_uint_good := to_uint tt.
   Notation to_uint' := (to_uint tt).
   Notation to_uint'' := (to_uint _).
@@ -254,8 +254,8 @@ Module Test14.
   Delimit Scope test14''_scope with test14''.
   Delimit Scope test14'''_scope with test14'''.
   Module Inner.
-    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
-    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Numeral.uint) : unit := tt.
     Local Numeral Notation unit of_uint to_uint : test14_scope.
     Global Numeral Notation unit of_uint to_uint : test14'_scope.
     Check let v := 0%test14 in v : unit.
@@ -267,8 +267,8 @@ Module Test14.
   Fail Check let v := 0%test14 in v : unit.
   Check let v := 0%test14' in v : unit.
   Section InnerSection.
-    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
-    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Numeral.uint) : unit := tt.
     Local Numeral Notation unit of_uint to_uint : test14''_scope.
     Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope.
     Check let v := 0%test14'' in v : unit.
@@ -283,8 +283,8 @@ Module Test15.
   Declare Scope test15_scope.
   Delimit Scope test15_scope with test15.
   Module Inner.
-    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
-    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Numeral.uint) : unit := tt.
     Numeral Notation unit of_uint to_uint : test15_scope.
     Check let v := 0%test15 in v : unit.
   End Inner.
@@ -306,8 +306,8 @@ Module Test16.
   End A.
   Module F (a : A).
     Inductive Foo := foo (_ : a.T).
-    Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O.
-    Definition of_uint (x : Decimal.uint) : Foo := foo a.t.
+    Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Numeral.uint) : Foo := foo a.t.
     Global Numeral Notation Foo of_uint to_uint : test16_scope.
     Check let v := 0%test16 in v : Foo.
   End F.
@@ -352,9 +352,9 @@ Module Test18.
   Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}.
   Definition nat_of_Q (x : Q) : option nat
     := if Nat.eqb x.(den) 1 then Some (x.(num)) else None.
-  Definition Q_of_uint (x : Decimal.uint) : Q := Q_of_nat (Nat.of_uint x).
-  Definition uint_of_Q (x : Q) : option Decimal.uint
-    := option_map Nat.to_uint (nat_of_Q x).
+  Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x).
+  Definition uint_of_Q (x : Q) : option Numeral.uint
+    := option_map Nat.to_num_uint (nat_of_Q x).
 
   Numeral Notation Q Q_of_uint uint_of_Q : Q_scope.
 
@@ -411,8 +411,8 @@ Module Test20.
 
   Record > ty := { t : Type ; kt : known_type t }.
 
-  Definition ty_of_uint (x : Decimal.uint) : option ty
-    := match Nat.of_uint x with
+  Definition ty_of_uint (x : Numeral.uint) : option ty
+    := match Nat.of_num_uint x with
        | 0 => @Some ty zero
        | 1 => @Some ty one
        | 2 => @Some ty two
@@ -421,8 +421,8 @@ Module Test20.
        | 5 => @Some ty type
        | _ => None
        end.
-  Definition uint_of_ty (x : ty) : Decimal.uint
-    := Nat.to_uint match kt x with
+  Definition uint_of_ty (x : ty) : Numeral.uint
+    := Nat.to_num_uint match kt x with
                    | prop => 3
                    | set => 4
                    | type => 5
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index fe6a1d25c6..9b5c076cb4 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -12,3 +12,15 @@ eq_refl : -1e-4 = -1e-4
      : -1e-4 = -1e-4
 eq_refl : -0.50 = -0.50
      : -0.50 = -0.50
+eq_refl : -26 = -26
+     : -26 = -26
+eq_refl : 2860 # 256 = 2860 # 256
+     : 2860 # 256 = 2860 # 256
+eq_refl : -6882 = -6882
+     : -6882 = -6882
+eq_refl : 2860 # 64 = 2860 # 64
+     : 2860 # 64 = 2860 # 64
+eq_refl : 2860 = 2860
+     : 2860 = 2860
+eq_refl : -2860 # 1024 = -2860 # 1024
+     : -2860 # 1024 = -2860 # 1024
diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v
index 2f2ee0134a..b5c6222bba 100644
--- a/test-suite/output/QArithSyntax.v
+++ b/test-suite/output/QArithSyntax.v
@@ -7,3 +7,9 @@ Check (eq_refl : 1.02e+02 = 102 # 1).
 Check (eq_refl : 10.2e-1 = 1.02).
 Check (eq_refl : -0.0001 = -1 # 10000).
 Check (eq_refl : -0.50 = - 50 # 100).
+Check (eq_refl : -0x1a = - 26 # 1).
+Check (eq_refl : 0xb.2c = 2860 # 256).
+Check (eq_refl : -0x1ae2 = -6882).
+Check (eq_refl : 0xb.2cp2 = 2860 # 64).
+Check (eq_refl : 0xb.2cp8 = 2860).
+Check (eq_refl : -0xb.2cp-2 = -2860 # 1024).
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 1685964b0f..a9386b2781 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -20,3 +20,18 @@ eq_refl : -1e-4 = -1e-4
      : -1e-4 = -1e-4
 eq_refl : -0.50 = -0.50
      : -0.50 = -0.50
+eq_refl : -26 = -26
+     : -26 = -26
+eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
+     : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
+eq_refl : -6882 = -6882
+     : -6882 = -6882
+eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
+     : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
+eq_refl : 2860 = 2860
+     : 2860 = 2860
+eq_refl
+:
+-2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10)
+     : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) =
+       - (2860) / IZR (Z.pow_pos 2 10)
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index e5f9d06316..69ce3ef5f9 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -14,6 +14,12 @@ Check (eq_refl : 1.02e+02 = IZR 102).
 Check (eq_refl : 10.2e-1 = 1.02).
 Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
 Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)).
+Check (eq_refl : -0x1a = - 26).
+Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)).
+Check (eq_refl : -0x1ae2 = -6882).
+Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)).
+Check (eq_refl : 0xb.2cp8 = 2860).
+Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)).
 
 Require Import Reals.
 
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 593d0c7f67..c01f4b2e19 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -21,57 +21,113 @@ le_sind:
 (use "About" for full details on implicit arguments)
 false: bool
 true: bool
-eq_true: bool -> Prop
 is_true: bool -> Prop
+eq_true: bool -> Prop
 negb: bool -> bool
+xorb: bool -> bool -> bool
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
 implb: bool -> bool -> bool
-xorb: bool -> bool -> bool
-Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.even: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Nat.ltb: nat -> nat -> bool
-Nat.testbit: nat -> nat -> bool
+Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
 Nat.eqb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
+Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
+Hexadecimal.hexadecimal_beq:
+  Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
+Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
+Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
+Decimal.int_beq: Decimal.int -> Decimal.int -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+eq_true_rec_r:
+  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
+eq_true_rect_r:
+  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_ind_r:
   forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+bool_sind:
+  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
 eq_true_sind:
   forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
-eq_true_rec_r:
-  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
-eq_true_rect_r:
-  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
-bool_sind:
-  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
-Byte.to_bits:
-  Byte.byte ->
-  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Numeral.internal_uint_dec_bl1:
+  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_lb:
+  forall x y : Hexadecimal.hexadecimal,
+  x = y -> Hexadecimal.hexadecimal_beq x y = true
+Hexadecimal.internal_int_dec_lb0:
+  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
+Numeral.internal_numeral_dec_lb:
+  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Hexadecimal.internal_int_dec_bl0:
+  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
+Numeral.internal_int_dec_lb1:
+  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Numeral.internal_int_dec_bl1:
+  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Numeral.internal_uint_dec_lb1:
+  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Decimal.internal_int_dec_bl:
+  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
+Decimal.internal_int_dec_lb:
+  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
+Numeral.internal_numeral_dec_bl:
+  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Hexadecimal.internal_uint_dec_bl0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-BoolSpec_sind:
-  forall [P Q : Prop] (P0 : bool -> SProp),
-  (P -> P0 true) ->
-  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 BoolSpec_ind:
   forall [P Q : Prop] (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
+BoolSpec_sind:
+  forall [P Q : Prop] (P0 : bool -> SProp),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 Byte.to_bits_of_bits:
   forall
     b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
@@ -107,14 +163,106 @@ f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
 (use "About" for full details on implicit arguments)
+Numeral.internal_numeral_dec_lb:
+  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Numeral.internal_int_dec_lb1:
+  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Numeral.internal_numeral_dec_bl:
+  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_lb:
+  forall x y : Hexadecimal.hexadecimal,
+  x = y -> Hexadecimal.hexadecimal_beq x y = true
+Numeral.internal_int_dec_bl1:
+  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Numeral.internal_uint_dec_lb1:
+  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Numeral.internal_uint_dec_bl1:
+  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Hexadecimal.internal_int_dec_lb0:
+  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
+Hexadecimal.internal_int_dec_bl0:
+  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
+Decimal.internal_int_dec_lb:
+  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Decimal.internal_int_dec_bl:
+  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
+Hexadecimal.internal_uint_dec_bl0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
   forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
 (use "About" for full details on implicit arguments)
+Numeral.internal_numeral_dec_lb:
+  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Numeral.internal_numeral_dec_bl:
+  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Numeral.internal_int_dec_lb1:
+  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Numeral.internal_int_dec_bl1:
+  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Numeral.internal_uint_dec_lb1:
+  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Numeral.internal_uint_dec_bl1:
+  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_lb:
+  forall x y : Hexadecimal.hexadecimal,
+  x = y -> Hexadecimal.hexadecimal_beq x y = true
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Hexadecimal.internal_int_dec_lb0:
+  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
+Hexadecimal.internal_int_dec_bl0:
+  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Decimal.internal_int_dec_lb:
+  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
+Decimal.internal_int_dec_bl:
+  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
+Hexadecimal.internal_uint_dec_bl0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 5627e4bd3c..d42dc575c2 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -8,16 +8,26 @@ le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
 true: bool
 negb: bool -> bool
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
-andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-Nat.even: nat -> bool
+andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 Nat.odd: nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+Hexadecimal.hexadecimal_beq:
+  Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
+Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
+Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
+Decimal.int_beq: Decimal.int -> Decimal.int -> bool
+Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 (use "About" for full details on implicit arguments)
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 36fc1a5914..13d0a9e55b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,47 +1,61 @@
 false: bool
 true: bool
 negb: bool -> bool
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
-andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-Nat.even: nat -> bool
+andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 Nat.odd: nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+Hexadecimal.hexadecimal_beq:
+  Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
+Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
+Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
+Decimal.int_beq: Decimal.int -> Decimal.int -> bool
+Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 (use "About" for full details on implicit arguments)
 Nat.two: nat
-Nat.one: nat
 Nat.zero: nat
+Nat.one: nat
 O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
 Nat.div2: nat -> nat
 Nat.log2: nat -> nat
-Nat.succ: nat -> nat
-Nat.sqrt: nat -> nat
-S: nat -> nat
 Nat.pred: nat -> nat
-Nat.double: nat -> nat
 Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.tail_mul: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.pow: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Hexadecimal.nb_digits: Hexadecimal.uint -> nat
+Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.of_num_uint: Numeral.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
 Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
@@ -53,29 +67,30 @@ Nat.div2: nat -> nat
 Nat.sqrt: nat -> nat
 Nat.log2: nat -> nat
 Nat.double: nat -> nat
-Nat.pred: nat -> nat
+S: nat -> nat
 Nat.square: nat -> nat
 Nat.succ: nat -> nat
-S: nat -> nat
+Nat.pred: nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.pow: nat -> nat -> nat
-Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
-Nat.tail_mul: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
+Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 (use "About" for full details on implicit arguments)
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index dc41b0aa48..c3f2fb5b42 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -1,5 +1,7 @@
 32%Z
      : Z
+eq_refl : 42%Z = 42%Z
+     : 42%Z = 42%Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
 fun x : positive => Z.pos x~0
@@ -24,3 +26,9 @@ Z.of_nat 0 = 0%Z
      : Prop
 (0 + Z.of_nat 11)%Z
      : Z
+0x2a%Z
+     : Z
+(-0x2a)%Z
+     : Z
+0x0%Z
+     : Z
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index d3640cae44..be9dc543d6 100644
--- a/test-suite/output/ZSyntax.v
+++ b/test-suite/output/ZSyntax.v
@@ -1,5 +1,6 @@
 Require Import ZArith.
 Check 32%Z.
+Check (eq_refl : 0x2a%Z = 42%Z).
 Check (fun f : nat -> Z => (f 0%nat + 0)%Z).
 Check (fun x : positive => Zpos (xO x)).
 Check (fun x : positive => (Zpos x + 1)%Z).
@@ -15,3 +16,10 @@ Check (Z.of_nat 0 = 0%Z).
 (* Submitted by Pierre Casteran *)
 Require Import Arith.
 Check (0 + Z.of_nat 11)%Z.
+
+(* Check hexadecimal printing *)
+Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n).
+Numeral Notation Z Z.of_num_int to_num_int : Z_scope.
+Check 42%Z.
+Check (-42)%Z.
+Check 0%Z.
diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
index 91d66f7f4c..6ea90eab29 100644
--- a/test-suite/output/bug_12159.v
+++ b/test-suite/output/bug_12159.v
@@ -2,10 +2,10 @@ Declare Scope A.
 Declare Scope B.
 Delimit Scope A with A.
 Delimit Scope B with B.
-Definition to_unit (v : Decimal.uint) : option unit
-  := match Nat.of_uint v with O => Some tt | _ => None end.
-Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
-Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1.
+Definition to_unit (v : Numeral.uint) : option unit
+  := match Nat.of_num_uint v with O => Some tt | _ => None end.
+Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
+Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1.
 Numeral Notation unit to_unit of_unit : A.
 Numeral Notation unit to_unit of_unit' : B.
 Definition f x : unit := x.