Merge PR #12218: Numeral notations for non inductive types

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

15 files changed, 1176 insertions, 182 deletions

diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6dadd8c7fe..84913abcdc 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -124,7 +124,7 @@ Check r 2 3.
 End I.
 
 Require Import Coq.Numbers.Cyclic.Int63.Int63.
-Module NumeralNotations.
+Module NumberNotations.
   Module Test17.
     (** Test int63 *)
     Declare Scope test17_scope.
@@ -134,7 +134,7 @@ Module NumeralNotations.
     Number Notation myint63 of_int to_int : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
-End NumeralNotations.
+End NumberNotations.
 
 Module K.
 
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 8065c8d311..60682edec8 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -1,9 +1,9 @@
 The command has indeed failed with message:
-Unexpected term (nat -> nat) while parsing a numeral notation.
+Unexpected term (nat -> nat) while parsing a number notation.
 The command has indeed failed with message:
-Unexpected non-option term opaque4 while parsing a numeral notation.
+Unexpected non-option term opaque4 while parsing a number notation.
 The command has indeed failed with message:
-Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral
+Unexpected term (fun (A : Type) (x : A) => x) while parsing a number
 notation.
 let v := 0%ppp in v : punit
      : punit
@@ -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 (Numeral.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 := Numeral.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 (Numeral.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
@@ -234,3 +234,282 @@ let v : ty := Build_ty Type type in v : ty
      : Prop
 1_000
      : list nat
+0
+     : Set
+1
+     : Set
+2
+     : Set
+3
+     : Set
+Empty_set
+     : Set
+unit
+     : Set
+sum unit unit
+     : Set
+sum unit (sum unit unit)
+     : Set
+The command has indeed failed with message:
+Missing mapping for constructor Isum.
+The command has indeed failed with message:
+Iunit was already mapped to unit and cannot be remapped to unit.
+The command has indeed failed with message:
+add is not an inductive type.
+The command has indeed failed with message:
+add is not a constructor of an inductive type.
+The command has indeed failed with message:
+Missing mapping for constructor Iempty.
+File "stdin", line 574, characters 56-61:
+Warning: Type of I'sum seems incompatible with the type of sum.
+Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+File "stdin", line 579, characters 32-33:
+Warning: I was already mapped to Set, mapping it also to
+nat might yield ill typed terms when using the notation.
+[via-type-remapping,numbers]
+File "stdin", line 579, characters 37-42:
+Warning: Type of Iunit seems incompatible with the type of O.
+Expected type is: I instead of I.
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+The command has indeed failed with message:
+'via' and 'abstract' cannot be used together.
+File "stdin", line 659, characters 21-23:
+Warning: Type of I1 seems incompatible with the type of Fin.F1.
+Expected type is: (nat -> I) instead of I.
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+File "stdin", line 659, characters 35-37:
+Warning: Type of IS seems incompatible with the type of Fin.FS.
+Expected type is: (nat -> I -> I) instead of (I -> I).
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+The command has indeed failed with message:
+The term "0" has type "forall n : nat, Fin.t (S n)"
+while it is expected to have type "nat".
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
+0
+     : list unit
+1
+     : list unit
+2
+     : list unit
+2
+     : list unit
+0 :: 0 :: nil
+     : list nat
+0
+     : Ip nat bool
+1
+     : Ip nat bool
+2
+     : Ip nat bool
+3
+     : Ip nat bool
+1
+     : Ip nat bool
+1
+     : Ip nat bool
+1
+     : Ip nat bool
+1
+     : Ip nat bool
+Ip0 nat nat 1
+     : Ip nat nat
+Ip0 bool bool 1
+     : Ip bool bool
+Ip1 nat nat 1
+     : Ip nat nat
+Ip3 1 nat nat
+     : Ip nat nat
+Ip0 nat bool O
+     : Ip nat bool
+Ip1 bool nat (S O)
+     : Ip nat bool
+Ip2 nat (S (S O)) bool
+     : Ip nat bool
+Ip3 (S (S (S O))) nat bool
+     : Ip nat bool
+0
+     : 0 = 0
+eq_refl
+     : 1 = 1
+0
+     : 1 = 1
+2
+     : extra_list_unit
+cons O unit tt (cons O unit tt (nil O unit))
+     : extra_list unit
+0
+     : Set
+1
+     : Set
+2
+     : Set
+3
+     : Set
+Empty_set
+     : Set
+unit
+     : Set
+sum unit unit
+     : Set
+sum unit (sum unit unit)
+     : Set
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat : Set]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat : Set]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat : Set]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat : Set]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat : Set]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat : Set]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat : Set]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat : Set]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index e411005da3..718da13500 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.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 : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
-  Number Notation Numeral.int opaque3 opaque3 : opaque_scope.
+  Definition opaque3 (x : Number.int) : Number.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
+  Number Notation Number.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 Numeral.int.
-  Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4.
-  Number Notation Numeral.int opaque6 opaque6 : opaque_scope.
+  Axiom opaque4 : option Number.int.
+  Definition opaque6 (x : Number.int) : option Number.int := opaque4.
+  Number Notation Number.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 : Numeral.uint) (f : forall A, A -> A).
-  Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x).
+  Inductive silly := SILLY (v : Number.uint) (f : forall A, A -> A).
+  Definition to_silly (v : Number.uint) := SILLY v (fun _ x => x).
   Definition of_silly (v : silly) := match v with SILLY v _ => v end.
   Number 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 : 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.
+  Polymorphic Definition pto_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pto_punit_all (v : Number.uint) : punit := ptt.
+  Polymorphic Definition pof_punit (v : punit) : Number.uint := Nat.to_num_uint 0.
+  Definition to_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end.
+  Definition of_punit (v : punit) : Number.uint := Nat.to_num_uint 0.
+  Polymorphic Definition pto_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Polymorphic Definition pof_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
+  Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
   Number Notation punit to_punit of_punit : pto.
   Number Notation punit pto_punit of_punit : ppo.
   Number Notation punit to_punit pof_punit : ptp.
@@ -83,7 +83,7 @@ Module Test4.
 
   Polymorphic Definition pto_punits := pto_punit_all@{Set}.
   Polymorphic Definition pof_punits := pof_punit@{Set}.
-  Number Notation punit pto_punits pof_punits : ppps (abstract after 1).
+  Number Notation punit pto_punits pof_punits (abstract after 1) : ppps.
   Delimit Scope ppps with ppps.
   Universe u.
   Constraint Set < u.
@@ -96,7 +96,7 @@ Module Test5.
 End Test5.
 
 Module Test6.
-  (* Check that numeral notations on enormous terms don't take forever to print/parse *)
+  (* Check that number notations on enormous terms don't take forever to print/parse *)
   (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *)
   Fixpoint ack (n m : nat) : nat :=
     match n with
@@ -113,15 +113,15 @@ Module Test6.
 
   Local Set Primitive Projections.
   Record > wnat := wrap { unwrap :> nat }.
-  Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x.
-  Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x.
+  Definition to_uint (x : wnat) : Number.uint := Nat.to_num_uint x.
+  Definition of_uint (x : Number.uint) : wnat := Nat.of_num_uint x.
   Module Export Scopes.
     Declare Scope wnat_scope.
     Delimit Scope wnat_scope with wnat.
   End Scopes.
   Module Export Notations.
     Export Scopes.
-    Number Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
+    Number Notation wnat of_uint to_uint (abstract after 5000) : wnat_scope.
   End Notations.
   Set Printing Coercions.
   Check let v := 0%wnat in v : wnat.
@@ -138,7 +138,7 @@ End Test6_2.
 
 Module Test7.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Numeral.uint }.
+  Record wuint := wrap { unwrap : Number.uint }.
   Declare Scope wuint_scope.
   Delimit Scope wuint_scope with wuint.
   Number Notation wuint wrap unwrap : wuint_scope.
@@ -148,7 +148,7 @@ End Test7.
 
 Module Test8.
   Local Set Primitive Projections.
-  Record wuint := wrap { unwrap : Numeral.uint }.
+  Record wuint := wrap { unwrap : Number.uint }.
   Declare Scope wuint8_scope.
   Declare Scope wuint8'_scope.
   Delimit Scope wuint8_scope with wuint8.
@@ -177,7 +177,7 @@ Module Test9.
   Delimit Scope wuint9'_scope with wuint9'.
   Section with_let.
     Local Set Primitive Projections.
-    Record wuint := wrap { unwrap : Numeral.uint }.
+    Record wuint := wrap { unwrap : Number.uint }.
     Let wrap' := wrap.
     Let unwrap' := unwrap.
     Local Notation wrap'' := wrap.
@@ -194,26 +194,26 @@ 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_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.
+  Definition of_uint (v : Number.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Number.uint) := tt.
   Declare Scope unit_scope.
   Declare Scope unit2_scope.
   Delimit Scope unit_scope with unit.
   Delimit Scope unit2_scope with unit2.
-  Number Notation unit of_uint to_uint : unit_scope (abstract after 1).
+  Number Notation unit of_uint to_uint (abstract after 1) : unit_scope.
   Local Set Warnings Append "+abstract-large-number-no-op".
   (* Check that there is actually a warning here *)
-  Fail Number Notation unit of_uint to_uint : unit2_scope (abstract after 1).
+  Fail Number Notation unit of_uint to_uint (abstract after 1) : unit2_scope.
   (* Check that there is no warning here *)
-  Number Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
+  Number Notation unit of_any_uint to_uint (abstract after 1) : unit2_scope.
 End Test10.
 
 Module Test12.
-  (* Test for numeral notations on context variables *)
+  (* Test for number notations on context variables *)
   Declare Scope test12_scope.
   Delimit Scope test12_scope with test12.
   Section test12.
-    Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit).
+    Context (to_uint : unit -> Number.uint) (of_uint : Number.uint -> unit).
 
     Number Notation unit of_uint to_uint : test12_scope.
     Check let v := 1%test12 in v : unit.
@@ -221,15 +221,15 @@ Module Test12.
 End Test12.
 
 Module Test13.
-  (* Test for numeral notations on notations which do not denote references *)
+  (* Test for number notations on notations which do not denote references *)
   Declare Scope test13_scope.
   Declare Scope test13'_scope.
   Declare Scope test13''_scope.
   Delimit Scope test13_scope with test13.
   Delimit Scope test13'_scope with test13'.
   Delimit Scope test13''_scope with test13''.
-  Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O.
-  Definition of_uint (x : Numeral.uint) : unit := tt.
+  Definition to_uint (x y : unit) : Number.uint := Nat.to_num_uint O.
+  Definition of_uint (x : Number.uint) : unit := tt.
   Definition to_uint_good := to_uint tt.
   Notation to_uint' := (to_uint tt).
   Notation to_uint'' := (to_uint _).
@@ -242,7 +242,7 @@ Module Test13.
 End Test13.
 
 Module Test14.
-  (* Test that numeral notations follow [Import], not [Require], and
+  (* Test that number notations follow [Import], not [Require], and
      also test that [Local Number Notation]s do not escape modules
      nor sections. *)
   Declare Scope test14_scope.
@@ -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) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Local Number Notation unit of_uint to_uint : test14_scope.
     Global Number 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) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Local Number Notation unit of_uint to_uint : test14''_scope.
     Fail Global Number 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) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : unit := tt.
+    Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : unit := tt.
     Number 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) : Numeral.uint := Nat.to_num_uint O.
-    Definition of_uint (x : Numeral.uint) : Foo := foo a.t.
+    Definition to_uint (x : Foo) : Number.uint := Nat.to_num_uint O.
+    Definition of_uint (x : Number.uint) : Foo := foo a.t.
     Global Number Notation Foo of_uint to_uint : test16_scope.
     Check let v := 0%test16 in v : Foo.
   End F.
@@ -352,8 +352,8 @@ 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 : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x).
-  Definition uint_of_Q (x : Q) : option Numeral.uint
+  Definition Q_of_uint (x : Number.uint) : Q := Q_of_nat (Nat.of_num_uint x).
+  Definition uint_of_Q (x : Q) : option Number.uint
     := option_map Nat.to_num_uint (nat_of_Q x).
 
   Number Notation Q Q_of_uint uint_of_Q : Q_scope.
@@ -411,7 +411,7 @@ Module Test20.
 
   Record > ty := { t : Type ; kt : known_type t }.
 
-  Definition ty_of_uint (x : Numeral.uint) : option ty
+  Definition ty_of_uint (x : Number.uint) : option ty
     := match Nat.of_num_uint x with
        | 0 => @Some ty zero
        | 1 => @Some ty one
@@ -421,7 +421,7 @@ Module Test20.
        | 5 => @Some ty type
        | _ => None
        end.
-  Definition uint_of_ty (x : ty) : Numeral.uint
+  Definition uint_of_ty (x : ty) : Number.uint
     := Nat.to_num_uint match kt x with
                    | prop => 3
                    | set => 4
@@ -487,3 +487,488 @@ Check (-0)%Z.
 *)
 
 End Test22.
+
+(* Test the via ... mapping ... option *)
+Module Test23.
+
+Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
+
+Inductive I :=
+| Iempty : I
+| Iunit : I
+| Isum : I -> I -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => Iempty
+      | S O => Iunit
+      | S n => Isum Iunit (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | Iempty => O
+      | Iunit => 1
+      | Isum i1 i2 => f i1 + f i2
+      end in
+  Nat.to_num_uint (f x).
+
+Notation nSet := (Set) (only parsing).  (* needed as a reference is expected in Number Notation and Set is syntactically not a reference *)
+Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum])
+  : type_scope.
+
+Local Open Scope type_scope.
+
+Check Empty_set.
+Check unit.
+Check sum unit unit.
+Check sum unit (sum unit unit).
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Unset Printing All.
+
+(* Test error messages *)
+
+(* missing constructor *)
+Fail Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit])
+  : type_scope.
+
+(* duplicate constructor *)
+Fail Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum, unit => Iunit])
+  : type_scope.
+
+(* not an inductive *)
+Fail Number Notation nSet of_uint to_uint (via add
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum])
+  : type_scope.
+
+(* not a constructor *)
+Fail Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => add, sum => Isum])
+  : type_scope.
+
+(* put constructors of the wrong inductive ~~> missing constructors *)
+Fail Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => O, unit => S])
+  : type_scope.
+
+(* Test warnings *)
+
+(* wrong type *)
+Inductive I' :=
+| I'empty : 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.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.
+
+(* wrong type mapping *)
+Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, O => Iunit, sum => Isum])
+  : type_scope.
+
+(* incompatibility with abstract (but warning is fine) *)
+Fail Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum],
+  abstract after 12)
+  : type_scope.
+Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum],
+  warning after 12)
+  : type_scope.
+
+(* Test reduction of types when building the notation *)
+
+Inductive foo := bar : match (true <: bool) with true => nat -> foo | false => True end.
+
+Definition foo_of_uint (x : Number.uint) : foo := bar (Nat.of_num_uint x).
+Definition foo_to_uint (x : foo) : Number.uint :=
+  match x with
+  | bar x => Nat.to_num_uint x
+  end.
+
+Number Notation foo foo_of_uint foo_to_uint (via foo mapping [bar => bar])
+  : type_scope.
+
+Inductive foo' := bar' : let n := nat in n -> foo'.
+
+Definition foo'_of_uint (x : Number.uint) : foo' := bar' (Nat.of_num_uint x).
+Definition foo'_to_uint (x : foo') : Number.uint :=
+  match x with
+  | bar' x => Nat.to_num_uint x
+  end.
+
+Number Notation foo' foo'_of_uint foo'_to_uint (via foo' mapping [bar' => bar'])
+  : type_scope.
+
+Inductive foo'' := bar'' : (nat <: Type) -> (foo'' <: Type).
+
+Definition foo''_of_uint (x : Number.uint) : foo'' := bar'' (Nat.of_num_uint x).
+Definition foo''_to_uint (x : foo'') : Number.uint :=
+  match x with
+  | bar'' x => Nat.to_num_uint x
+  end.
+
+Number Notation foo'' foo''_of_uint foo''_to_uint (via foo'' mapping [bar'' => bar''])
+  : type_scope.
+
+End Test23.
+
+(* Test the via ... mapping ... option with implicit arguments *)
+Require Vector.
+Module Test24.
+
+Import Vector.
+
+Inductive I :=
+| I1 : I
+| IS : I -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+(* ignoring implicit arguments doesn't work *)
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [Fin.F1 => I1, Fin.FS => IS])
+  : type_scope.
+
+Fail Check 1.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test24.
+
+(* Test number notations for parameterized inductives *)
+Module Test25.
+
+Definition of_uint (u : Number.uint) : list unit :=
+  let fix f n :=
+    match n with
+    | O => nil
+    | S n => cons tt (f n)
+    end in
+  f (Nat.of_num_uint u).
+
+Definition to_uint (l : list unit) : Number.uint :=
+  let fix f n :=
+    match n with
+    | nil => O
+    | cons tt l => S (f l)
+    end in
+  Nat.to_num_uint (f l).
+
+Notation listunit := (list unit) (only parsing).
+Number Notation listunit of_uint to_uint : nat_scope.
+
+Check 0.
+Check 1.
+Check 2.
+
+Check cons tt (cons tt nil).
+Check cons O (cons O nil).  (* printer not called on list nat *)
+
+(* inductive with multiple parameters that are not the first
+   parameters and not in the same order for each constructor *)
+Inductive Ip : Type -> Type -> Type :=
+| Ip0 : forall T T', nat -> Ip T T'
+| Ip1 : forall T' T, nat -> Ip T T'
+| Ip2 : forall T, nat -> forall T', Ip T T'
+| Ip3 : nat -> forall T T', Ip T T'.
+
+Definition Ip_of_uint (u : Number.uint) : option (Ip nat bool) :=
+  let f n :=
+    match n with
+    | O => Some (Ip0 nat bool O)
+    | S O => Some (Ip1 bool nat (S O))
+    | S (S O) => Some (Ip2 nat (S (S O)) bool)
+    | S (S (S O)) => Some (Ip3 (S (S (S O))) nat bool)
+    | _ => None
+    end in
+  f (Nat.of_num_uint u).
+
+Definition Ip_to_uint (l : Ip nat bool) : Number.uint :=
+  let f n :=
+    match n with
+    | Ip0 _ _ n => n
+    | Ip1 _ _ n => n
+    | Ip2 _ n _ => n
+    | Ip3 n _ _ => n
+    end in
+  Nat.to_num_uint (f l).
+
+Notation Ip_nat_bool := (Ip nat bool) (only parsing).
+Number Notation Ip_nat_bool Ip_of_uint Ip_to_uint : nat_scope.
+
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check Ip0 nat bool (S O).
+Check Ip1 bool nat (S O).
+Check Ip2 nat (S O) bool.
+Check Ip3 (S O) nat bool.
+Check Ip0 nat nat (S O).  (* not printed *)
+Check Ip0 bool bool (S O).  (* not printed *)
+Check Ip1 nat nat (S O).  (* not printed *)
+Check Ip3 (S O) nat nat.  (* not printed *)
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Unset Printing All.
+
+Notation eqO := (eq _ O) (only parsing).
+Definition eqO_of_uint (x : Number.uint) : eqO := eq_refl O.
+Definition eqO_to_uint (x : O = O) : Number.uint :=
+  match x with
+  | eq_refl _ => Nat.to_num_uint O
+  end.
+Number Notation eqO eqO_of_uint eqO_to_uint : nat_scope.
+
+Check 42.
+Check eq_refl (S O).  (* doesn't match eq _ O, printer not called *)
+
+Notation eq_ := (eq _ _) (only parsing).
+Number Notation eq_ eqO_of_uint eqO_to_uint : nat_scope.
+
+Check eq_refl (S O).  (* matches eq _ _, printer called *)
+
+Inductive extra_list : Type -> Type :=
+| nil (n : nat) (v : Type) : extra_list v
+| cons (n : nat) (t : Type) (x : t) : extra_list t -> extra_list t.
+
+Definition extra_list_unit_of_uint (x : Number.uint) : extra_list unit :=
+  let fix f n :=
+      match n with
+      | O => nil O unit
+      | S n => cons O unit tt (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition extra_list_unit_to_uint (x : extra_list unit) : Number.uint :=
+  let fix f T (x : extra_list T) :=
+      match x with
+      | nil _ _ => O
+      | cons _ T _ x => S (f T x)
+      end in
+  Nat.to_num_uint (f unit x).
+
+Notation extra_list_unit := (extra_list unit).
+Number Notation extra_list_unit
+        extra_list_unit_of_uint extra_list_unit_to_uint : nat_scope.
+
+Check 2.
+Set Printing All.
+Check 2.
+Unset Printing All.
+
+End Test25.
+
+(* Test the via ... mapping ... option with let-binders, beta-redexes, delta-redexes, etc *)
+Module Test26.
+
+Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
+
+Inductive I (dummy:=O) :=
+| Iempty : let v := I in id v
+| Iunit : (fun x => x) I
+| Isum : let v := I in (fun A B => A -> B) (let v' := v in v') (forall x : match O with O => I | _ => Empty_set end, let dummy2 := x in I).
+
+Definition of_uint (x : (fun x => let v := I in x) Number.uint) : (fun x => let v := I in x) I :=
+  let fix f n :=
+      match n with
+      | O => Iempty
+      | S O => Iunit
+      | S n => Isum Iunit (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : (fun x => let v := x in v) I) : match O with O => Number.uint | _ => Empty_set end :=
+  let fix f i :=
+      match i with
+      | Iempty => O
+      | Iunit => 1
+      | Isum i1 i2 => f i1 + f i2
+      end in
+  Nat.to_num_uint (f x).
+
+Notation nSet := (Set) (only parsing).  (* needed as a reference is expected in Number Notation and Set is syntactically not a reference *)
+Number Notation nSet of_uint to_uint (via I
+  mapping [Empty_set => Iempty, unit => Iunit, sum => Isum])
+  : type_scope.
+
+Local Open Scope type_scope.
+
+Check Empty_set.
+Check unit.
+Check sum unit unit.
+Check sum unit (sum unit unit).
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Unset Printing All.
+End Test26.
+
+(* Test the via ... mapping ... option with implicit arguments with let binders, etc *)
+Module Test27.
+
+Module Fin.
+Inductive t0 (x:=O) :=
+with
+  t (x:=O) : forall y : nat, let z := y in Set :=
+| F1 (y:=O) {n} : match y with O => t (S n) | _ => Empty_set end
+| FS (y:=x) {n} (v:=n+y) (m:=n) : id (match y with O => id (t n) | _ => Empty_set end -> (fun x => x) t (S m))
+with t' (x:=O) := .
+End Fin.
+
+Inductive I (dummy:=O) :=
+| I1 : I
+| IS : let x := I in id x -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test27.
+
+Module Test28.
+Module Fin.
+Inductive t : nat -> Set :=
+| F1 {n : (nat : Set)} : (t (S n) : Set)
+| FS {n : (nat : Set)} : (t n : Set) -> (t (S n) : Set).
+End Fin.
+
+Inductive I :=
+| I1 : I
+| IS : I -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test28.
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index 9b5c076cb4..ced52524f2 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -1,26 +1,72 @@
 eq_refl : 1.02 = 1.02
      : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 1020 = 1020
-     : 1020 = 1020
-eq_refl : 102 = 102
-     : 102 = 102
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : -1e-4 = -1e-4
-     : -1e-4 = -1e-4
+1.02e1
+     : Q
+10.2
+     : Q
+1.02e3
+     : Q
+1020
+     : Q
+1.02e2
+     : Q
+102
+     : Q
+eq_refl : 10.2e-1 = 1.02
+     : 10.2e-1 = 1.02
+eq_refl : -0.0001 = -0.0001
+     : -0.0001 = -0.0001
 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
+0
+     : Q
+0
+     : Q
+42
+     : Q
+42
+     : Q
+1.23
+     : Q
+0x1.23%xQ
+     : Q
+0.0012
+     : Q
+42e3
+     : Q
+42e-3
+     : Q
+eq_refl : -0x1a = -0x1a
+     : -0x1a = -0x1a
+eq_refl : 0xb.2c = 0xb.2c
+     : 0xb.2c = 0xb.2c
+eq_refl : -0x1ae2 = -0x1ae2
+     : -0x1ae2 = -0x1ae2
+0xb.2cp2
+     : Q
+2860 # 64
+     : Q
+0xb.2cp8
+     : Q
+0xb2c
+     : Q
+eq_refl : -0xb.2cp-2 = -2860 # 1024
+     : -0xb.2cp-2 = -2860 # 1024
+0x0
+     : Q
+0x0
+     : Q
+0x2a
+     : Q
+0x2a
+     : Q
+1.23%Q
+     : Q
+0x1.23
+     : Q
+0x0.0012
+     : Q
+0x2ap3
+     : Q
+0x2ap-3
+     : Q
diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v
index b5c6222bba..e979abca66 100644
--- a/test-suite/output/QArithSyntax.v
+++ b/test-suite/output/QArithSyntax.v
@@ -1,15 +1,39 @@
 Require Import QArith.
 Open Scope Q_scope.
 Check (eq_refl : 1.02 = 102 # 100).
-Check (eq_refl : 1.02e1 = 102 # 10).
-Check (eq_refl : 1.02e+03 = 1020).
-Check (eq_refl : 1.02e+02 = 102 # 1).
+Check 1.02e1.
+Check 102 # 10.
+Check 1.02e+03.
+Check 1020.
+Check 1.02e+02.
+Check 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 0.
+Check 000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0.0012.
+Check 42e3.
+Check 42e-3.
+Open Scope hex_Q_scope.
 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 0xb.2cp2.
+Check 2860 # 64.
+Check 0xb.2cp8.
+Check 2860.
 Check (eq_refl : -0xb.2cp-2 = -2860 # 1024).
+Check 0x0.
+Check 0x00.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0x0.0012.
+Check 0x2ap3.
+Check 0x2ap-3.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index a9386b2781..a7b7dabb20 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -4,34 +4,81 @@
      : R
 1.5%R
      : R
-15%R
-     : R
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 102e1 = 102e1
-     : 102e1 = 102e1
-eq_refl : 102 = 102
-     : 102 = 102
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : -1e-4 = -1e-4
-     : -1e-4 = -1e-4
-eq_refl : -0.50 = -0.50
-     : -0.50 = -0.50
+1.5e1%R
+     : R
+eq_refl : 1.02 = 102e-2
+     : 1.02 = 102e-2
+1.02e1
+     : R
+102e-1
+     : R
+1.02e3
+     : R
+102e1
+     : R
+1.02e2
+     : R
+102
+     : R
+10.2e-1
+     : R
+1.02
+     : R
+eq_refl : -0.0001 = -1e-4
+     : -0.0001 = -1e-4
+eq_refl : -0.50 = -50e-2
+     : -0.50 = -50e-2
 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 : 0xb.2c%xR = 0xb2cp-8%xR
+     : 0xb.2c%xR = 0xb2cp-8%xR
 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)
+0xb.2cp2%xR
+     : R
+0xb2cp-6%xR
+     : R
+0xb.2cp8%xR
+     : R
+2860
+     : R
+(-0xb.2cp-2)%xR
+     : R
+- 0xb2cp-10%xR
+     : R
+0
+     : R
+0
+     : R
+42
+     : R
+42
+     : R
+1.23
+     : R
+0x1.23%xR
+     : R
+0.0012
+     : R
+42e3
+     : R
+42e-3
+     : R
+0x0
+     : R
+0x0
+     : R
+0x2a
+     : R
+0x2a
+     : R
+1.23%R
+     : R
+0x1.23
+     : R
+0x0.0012
+     : R
+0x2ap3
+     : R
+0x2ap-3
+     : R
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 69ce3ef5f9..790d5c654f 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -8,18 +8,48 @@ Check 1_.5_e1_%R.
 Open Scope R_scope.
 
 Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
-Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+02 = IZR 102).
-Check (eq_refl : 10.2e-1 = 1.02).
+Check 1.02e1.
+Check IZR 102 / IZR (Z.pow_pos 10 1).
+Check 1.02e+03.
+Check IZR 102 * IZR (Z.pow_pos 10 1).
+Check 1.02e+02.
+Check IZR 102.
+Check 10.2e-1.
+Check 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)).
+Check 0xb.2cp2.
+Check IZR 2860 / IZR (Z.pow_pos 2 6).
+Check 0xb.2cp8.
+Check 2860.
+Check -0xb.2cp-2.
+Check - (IZR 2860 / IZR (Z.pow_pos 2 10)).
+Check 0.
+Check 000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0.0012.
+Check 42e3.
+Check 42e-3.
+
+Open Scope hex_R_scope.
+
+Check 0x0.
+Check 0x000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0x0.0012.
+Check 0x2ap3.
+Check 0x2ap-3.
+
+Close Scope hex_R_scope.
 
 Require Import Reals.
 
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 09feca71e7..914e7f88c6 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -30,15 +30,15 @@ implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
+Number.number_beq: Number.number -> Number.number -> 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
+Number.uint_beq: Number.uint -> Number.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
+Number.int_beq: Number.int -> Number.int -> bool
 Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
@@ -64,34 +64,34 @@ eq_true_rec:
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_sind:
   forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.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
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_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
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.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
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.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
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
@@ -160,21 +160,21 @@ f_equal2_mult:
 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
-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
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_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
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.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:
@@ -213,18 +213,18 @@ 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}
-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
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.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
@@ -306,12 +306,12 @@ nat_rect_plus:
     (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) 
     (fun _ : nat => f) n
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Numeral.internal_numeral_dec_bl:
-  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
-Numeral.internal_int_dec_bl1:
-  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
-Numeral.internal_uint_dec_bl1:
-  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
+Number.internal_int_dec_bl1:
+  forall x y : Number.int, Number.int_beq x y = true -> x = y
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_bl:
   forall x y : Hexadecimal.hexadecimal,
   Hexadecimal.hexadecimal_beq x y = true -> x = y
@@ -328,12 +328,12 @@ Byte.to_bits_of_bits:
   forall
     b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
   Byte.to_bits (Byte.of_bits b) = b
-Numeral.internal_numeral_dec_lb:
-  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
-Numeral.internal_uint_dec_lb1:
-  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
-Numeral.internal_int_dec_lb1:
-  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Number.internal_int_dec_lb1:
+  forall x y : Number.int, x = y -> Number.int_beq x y = true
 Decimal.internal_int_dec_lb:
   forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
 Hexadecimal.internal_hexadecimal_dec_lb:
@@ -391,7 +391,7 @@ Nat.lor: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
 Nat.of_hex_uint: Hexadecimal.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
-Nat.of_num_uint: Numeral.uint -> nat
+Nat.of_num_uint: Number.uint -> nat
 length: forall [A : Type], list A -> nat
 plus_n_O: forall n : nat, n = n + 0
 plus_O_n: forall n : nat, 0 + n = n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 9554581ebe..2f0d854ac6 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -21,15 +21,15 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
-Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Number.uint_beq: Number.uint -> Number.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
+Number.number_beq: Number.number -> Number.number -> bool
+Number.int_beq: Number.int -> Number.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
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 80b03e8a0b..d705ec898b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -7,15 +7,15 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
-Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
+Number.uint_beq: Number.uint -> Number.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
+Number.number_beq: Number.number -> Number.number -> bool
+Number.int_beq: Number.int -> Number.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
@@ -50,7 +50,7 @@ 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_num_uint: Number.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
 Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index e9cf4282dc..68ee7cfeb5 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -1051,7 +1051,7 @@ Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
 "127"
      : byte
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : ascii
 "a"
@@ -1059,7 +1059,7 @@ Expects a single character or a three-digits ascii code.
 "127"
      : ascii
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : string
 "a"
@@ -1084,3 +1084,21 @@ Expects a single character or a three-digits ascii code.
      = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167";
        "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"]
      : list ascii
+"abc"
+     : string
+"000"
+     : nat
+"001"
+     : nat
+"002"
+     : nat
+"255"
+     : nat
+The command has indeed failed with message:
+Expects a single character or a three-digit ASCII code.
+"abc"
+     : string2
+"abc" : string2
+     : string2
+"abc" : string1
+     : string1
diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
index aab6e0bb03..a1ffe69527 100644
--- a/test-suite/output/StringSyntax.v
+++ b/test-suite/output/StringSyntax.v
@@ -50,3 +50,68 @@ Local Close Scope byte_scope.
 Local Open Scope char_scope.
 Compute List.map Ascii.ascii_of_nat (List.seq 0 256).
 Local Close Scope char_scope.
+
+(* Test numeral notations for parameterized inductives *)
+Module Test2.
+
+Notation string := (list Byte.byte).
+Definition id_string := @id string.
+
+String Notation string id_string id_string : list_scope.
+
+Check "abc"%list.
+
+End Test2.
+
+(* Test the via ... using ... option *)
+Module Test3.
+
+Inductive I :=
+| IO : I
+| IS : I -> I.
+
+Definition of_byte (x : Byte.byte) : I :=
+  let fix f n :=
+      match n with
+      | O => IO
+      | S n => IS (f n)
+      end in
+  f (Byte.to_nat x).
+
+Definition to_byte (x : I) : option Byte.byte :=
+  let fix f i :=
+      match i with
+      | IO => O
+      | IS i => S (f i)
+      end in
+  Byte.of_nat (f x).
+
+String Notation nat of_byte to_byte (via I mapping [O => IO, S => IS]) : nat_scope.
+
+Check "000".
+Check "001".
+Check "002".
+Check "255".
+Fail Check "256".
+
+End Test3.
+
+(* Test overlapping string notations *)
+Module Test4.
+
+Notation string1 := (list Byte.byte).
+Definition id_string1 := @id string1.
+
+String Notation string1 id_string1 id_string1 : list_scope.
+
+Notation string2 := (list Ascii.ascii).
+Definition a2b := List.map byte_of_ascii.
+Definition b2a := List.map ascii_of_byte.
+
+String Notation string2 b2a a2b : list_scope.
+
+Check "abc"%list.
+Check ["a";"b";"c"]%char%list : string2.
+Check ["a";"b";"c"]%byte%list : string1.
+
+End Test4.
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index 7b2bb00ce0..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 := Numeral.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/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
index 437b4a68e9..a7366f2d35 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 : Numeral.uint) : option unit
+Definition to_unit (v : Number.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.
+Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
+Definition of_unit' (v : unit) : Number.uint := Nat.to_num_uint 1.
 Number Notation unit to_unit of_unit : A.
 Number Notation unit to_unit of_unit' : B.
 Definition f x : unit := x.
diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumberNotationsNoLocal.v
index fe97f10ddf..e19d06cfa7 100644
--- a/test-suite/success/NumeralNotationsNoLocal.v
+++ b/test-suite/success/NumberNotationsNoLocal.v
@@ -1,4 +1,4 @@
-(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+(* Test that number notations don't work on proof-local variables, especially not ones containing evars *)
 Inductive unit11 := tt11.
 Declare Scope unit11_scope.
 Delimit Scope unit11_scope with unit11.