Merge PR #11703: Making of NumTok an API for numeral

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01

36 files changed, 677 insertions, 281 deletions

diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
new file mode 100644
index 0000000000..8a734feada
--- /dev/null
+++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
+
+    quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b82388675c..eac8d86b0a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -11,6 +11,8 @@
 
 Notations:
 
+- Most operators on numerals have moved to file numTok.ml.
+
 - Types `precedence`, `parenRelation`, `tolerability` in
   `notgram_ops.ml` have been reworked. See `entry_level` and
   `entry_relative_level` in `constrexpr.ml`.
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index da224aa5ab..06db787488 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -24,6 +24,8 @@ install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
 install_printer Top_printers.ppbigint
+install_printer Top_printers.ppnumtokunsigned
+install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
 install_printer Top_printers.ppidset
 install_printer Top_printers.ppidmapgen
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 96dbf9142b..7002cbffac 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -86,6 +86,8 @@ let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x)
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
+let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
+let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
 let ppintset l = pp (prset int (Int.Set.elements l))
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c5f97f5873..c826391cac 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -54,6 +54,8 @@ val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
 
 val ppbigint : Bigint.bigint -> unit
+val ppnumtokunsigned : NumTok.Unsigned.t -> unit
+val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
 
 val ppintset : Int.Set.t -> unit
 val ppidset : Names.Id.Set.t -> unit
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 8732b0e2c6..21f682ac0e 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -57,26 +57,8 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
-(** Representation of decimal literals that appear in Coq scripts.
-   We now use raw strings following the format defined by
-   [NumTok.t] and a separate sign flag.
-
-   Note that this representation is not unique, due to possible
-   multiple leading or trailing zeros, and -0 = +0, for instances.
-   The reason to keep the numeral exactly as it was parsed is that
-   specific notations can be declared for specific numerals
-   (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
-   [Notation "2e1" := ...]). Those notations, which override the
-   generic interpretation as numeral, use the same representation of
-   numeral using the Numeral constructor. So the latter should be able
-   to record the form of the numeral which exactly matches the
-   notation. *)
-
-type sign = SPlus | SMinus
-type raw_numeral = NumTok.t
-
 type prim_token =
-  | Numeral of sign * raw_numeral
+  | Numeral of NumTok.Signed.t
   | String of string
 
 type instance_expr = Glob_term.glob_level list
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index da5b8d9132..d4369e9bd1 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -48,10 +48,9 @@ let names_of_local_binders bl =
    are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral (SPlus,n1), Numeral (SPlus,n2)
-| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2
+| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2
 | String s1, String s2 -> String.equal s1 s2
-| (Numeral ((SPlus|SMinus),_) | String _), _ -> false
+| (Numeral _ | String _), _ -> false
 
 let explicitation_eq ex1 ex2 = match ex1, ex2 with
 | ExplByPos (i1, id1), ExplByPos (i2, id2) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a16825b5c9..7a14ca3e48 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -354,27 +354,21 @@ let drop_implicits_in_patt cst nb_expl args =
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
-let is_zero s =
-  let rec aux i =
-    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
-  in aux 0
-let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
-
 let make_notation_gen loc ntn mknot mkprim destprim l bl =
   match snd ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) ->
+    | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
         assert (bl=[]);
         mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
         | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
-           begin match NumTok.of_string x with
-           | Some n -> mkprim (loc, Numeral (SMinus,n))
+           begin match NumTok.Unsigned.parse_string x with
+           | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | (InConstrEntrySomeLevel,[Terminal x]), [] ->
-           begin match NumTok.of_string x with
-           | Some n -> mkprim (loc, Numeral (SPlus,n))
+           begin match NumTok.Unsigned.parse_string x with
+           | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
@@ -899,13 +893,10 @@ let extern_float f scopes =
   else if Float64.is_infinity f then CRef(q_infinity (), None)
   else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
   else
-    let sign = if Float64.sign f then SMinus else SPlus in
-    let s = Float64.(to_string (abs f)) in
-    match NumTok.of_string s with
-    | None -> assert false
-    | Some n ->
-       extern_prim_token_delimiter_if_required (Numeral (sign, n))
-       "float" "float_scope" scopes
+    let s = Float64.(to_string f) in
+    let n = NumTok.Signed.of_string s in
+    extern_prim_token_delimiter_if_required (Numeral n)
+      "float" "float_scope" scopes
 
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
@@ -1085,7 +1076,7 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GInt i ->
      extern_prim_token_delimiter_if_required
-       (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+       (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
   | GFloat f -> extern_float f (snd scopes)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index abacadc43a..a071ba7ec9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,7 @@ open Notation_ops
 open Notation
 open Inductiveops
 open Context.Rel.Declaration
+open NumTok
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
@@ -1585,12 +1586,6 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let is_zero s =
-  let rec aux i =
-    Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1))
-  in aux 0
-let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
-
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
@@ -1614,11 +1609,11 @@ let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
 let is_non_zero c = match c with
-| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p)
+| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p)
+| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
diff --git a/interp/notation.ml b/interp/notation.ml
index 4b73189ad3..6291a88bb0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -21,6 +21,7 @@ open Notation_term
 open Glob_term
 open Glob_ops
 open Context.Named.Declaration
+open NumTok
 
 (*i*)
 
@@ -335,7 +336,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
 type required_module = full_path * string list
-type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
+type rawnum = NumTok.Signed.t
 
 type prim_token_uid = string
 
@@ -358,17 +359,13 @@ module InnerPrimToken = struct
     | StringInterp f, StringInterp f' -> f == f'
     | _ -> false
 
-  let ofNumeral s n =
-    let n = String.(concat "" (split_on_char '_' n)) in
-    match s with
-    | SPlus -> Bigint.of_string n
-    | SMinus -> Bigint.neg (Bigint.of_string n)
-
   let do_interp ?loc interp primtok =
     match primtok, interp with
-    | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n)
-    | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }),
-      BigNumInterp interp -> interp ?loc (ofNumeral s n)
+    | Numeral n, RawNumInterp interp -> interp ?loc n
+    | Numeral n, BigNumInterp interp ->
+      (match NumTok.Signed.to_bigint n with
+       | Some n -> interp ?loc n
+       | None -> raise Not_found)
     | String s, StringInterp interp -> interp ?loc s
     | (Numeral _ | String _),
       (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
@@ -385,10 +382,7 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    if Bigint.is_pos_or_zero n then
-      Numeral (SPlus,NumTok.int (Bigint.to_string n))
-    else
-      Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg n)))
+    Numeral (NumTok.Signed.of_bigint n)
 
   let mkString = function
     | None -> None
@@ -425,8 +419,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of string
-  | Abstract of string
+  | Warning of NumTok.UnsignedNat.t
+  | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
   { uint : Names.inductive;
@@ -567,7 +561,7 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
     Some (to_raw (fst o.of_kind, c))
   with
   | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
-  | NotAValidPrimToken -> None (* all other functions except big2raw *)
+  | NotAValidPrimToken -> None (* all other functions except NumTok.Signed.of_bigint *)
 
 end
 
@@ -600,26 +594,6 @@ let warn_abstract_large_num =
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
 
-(** Comparing two raw numbers (base 10, big-endian, non-negative).
-    A bit nasty, but not critical: only used to decide when a
-    number is considered as large (see warnings above). *)
-
-exception Comp of int
-
-let rec rawnum_compare s s' =
- let l = String.length s and l' = String.length s' in
- if l < l' then - rawnum_compare s' s
- else
-   let d = l-l' in
-   try
-     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
-     for i = d to l-1 do
-       let c = pervasives_compare s.[i] s'.[i-d] in
-       if c != 0 then raise (Comp c)
-     done;
-     0
-   with Comp c -> c
-
 (***********************************************************************)
 
 (** ** Conversion between Coq [Decimal.int] and internal raw string *)
@@ -634,32 +608,31 @@ let char_of_digit n =
   assert (2<=n && n<=11);
   Char.chr (n-2 + Char.code '0')
 
-let coquint_of_rawnum uint str =
+let coquint_of_rawnum uint n =
   let nil = mkConstruct (uint,1) in
+  match n with None -> nil | Some n ->
+  let str = NumTok.UnsignedNat.to_string n in
   let rec do_chars s i acc =
     if i < 0 then acc
-    else if s.[i] == '_' then do_chars s (i-1) acc else
+    else
       let dg = mkConstruct (uint, digit_of_char s.[i]) in
       do_chars s (i-1) (mkApp(dg,[|acc|]))
   in
   do_chars str (String.length str - 1) nil
 
-let coqint_of_rawnum inds sign str =
-  let uint = coquint_of_rawnum inds.uint str in
+let coqint_of_rawnum inds (sign,n) =
+  let uint = coquint_of_rawnum inds.uint (Some n) in
   let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
   mkApp (mkConstruct (inds.int, pos_neg), [|uint|])
 
-let coqdecimal_of_rawnum inds sign n =
-  let i, f, e = NumTok.(n.int, n.frac, n.exp) in
-  let i = coqint_of_rawnum inds.int sign i in
+let coqdecimal_of_rawnum inds n =
+  let i, f, e = NumTok.Signed.to_decimal_and_exponent n in
+  let i = coqint_of_rawnum inds.int i in
   let f = coquint_of_rawnum inds.int.uint f in
-  if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|])  (* Decimal *)
-  else
-    let sign, e = match e.[1] with
-      | '-' -> SMinus, String.sub e 2 (String.length e - 2)
-      | '+' -> SPlus, String.sub e 2 (String.length e - 2)
-      | _ -> SPlus, String.sub e 1 (String.length e - 1) in
-    let e = coqint_of_rawnum inds.int sign e in
+  match e with
+  | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|])  (* Decimal *)
+  | Some e ->
+    let e = coqint_of_rawnum inds.int e in
     mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|])  (* DecimalExp *)
 
 let rawnum_of_coquint c =
@@ -680,26 +653,23 @@ let rawnum_of_coquint c =
     (* To avoid ambiguities between Nil and (D0 Nil), we choose
        to not display Nil alone as "0" *)
     raise NotAValidPrimToken
-  else NumTok.int (Buffer.contents buf)
+  else NumTok.UnsignedNat.of_string (Buffer.contents buf)
 
 let rawnum_of_coqint c =
   match Constr.kind c with
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c')
-      | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c')
+      | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c')
+      | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c')
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
 let rawnum_of_decimal c =
   let of_ife i f e =
-    let sign, n = rawnum_of_coqint i in
-    let f =
-      try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in
-    let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with
-      | SPlus, e -> "e+" ^ e.NumTok.int
-      | SMinus, e -> "e-" ^ e.NumTok.int in
-    sign,{ n with NumTok.frac = f; exp = e } in
+    let n = rawnum_of_coqint i in
+    let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in
+    let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in
+    NumTok.Signed.of_decimal_and_exponent n f e in
   match Constr.kind c with
   | App (_,[|i; f|]) -> of_ife i f None
   | App (_,[|i; f; e|]) -> of_ife i f (Some e)
@@ -789,43 +759,31 @@ let bigint_of_int63 c =
   | Int i -> Bigint.of_string (Uint63.to_string i)
   | _ -> raise NotAValidPrimToken
 
-let big2raw n =
-  if Bigint.is_pos_or_zero n then
-    (SPlus, NumTok.int (Bigint.to_string n))
-  else
-    (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n)))
-
-let raw2big s n = match s with
-  | SPlus -> Bigint.of_string n
-  | SMinus -> Bigint.neg (Bigint.of_string n)
-
 let interp o ?loc n =
   begin match o.warning, n with
-  | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" })
-       when rawnum_compare n threshold >= 0 ->
+  | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_large_num o.ty_name
   | _ -> ()
   end;
-  let c = match fst o.to_kind, n with
-    | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       coqint_of_rawnum int_ty s n
-    | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) ->
-       coquint_of_rawnum uint_ty n
-    | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       z_of_bigint z_pos_ty (raw2big s n)
-    | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       interp_int63 ?loc (raw2big s n)
+  let c = match fst o.to_kind, NumTok.Signed.to_int n with
+    | Int int_ty, Some n ->
+       coqint_of_rawnum int_ty n
+    | UInt uint_ty, Some (SPlus, n) ->
+       coquint_of_rawnum uint_ty (Some n)
+    | Z z_pos_ty, Some n ->
+       z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
+    | Int63, Some n ->
+       interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
     | (Int _ | UInt _ | Z _ | Int63), _ ->
        no_such_prim_token "number" ?loc o.ty_name
-    | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n
+    | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
   let to_ty = EConstr.Unsafe.to_constr to_ty in
   match o.warning, snd o.to_kind with
-  | Abstract threshold, Direct
-       when rawnum_compare (snd n).NumTok.int threshold >= 0 ->
+  | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
      glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
@@ -837,10 +795,10 @@ let interp o ?loc n =
 let uninterp o n =
   PrimTokenNotation.uninterp
     begin function
-      | (Int _, c) -> rawnum_of_coqint c
-      | (UInt _, c) -> (SPlus, rawnum_of_coquint c)
-      | (Z _, c) -> big2raw (bigint_of_z c)
-      | (Int63, c) -> big2raw (bigint_of_int63 c)
+      | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
+      | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
+      | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c)
+      | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c)
       | (Decimal _, c) -> rawnum_of_decimal c
     end o n
 end
@@ -1162,8 +1120,8 @@ let find_notation ntn sc =
   NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
-  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
-  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n
+  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
+  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
diff --git a/interp/notation.mli b/interp/notation.mli
index 8fcf9dc5dc..892eba8d11 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -81,7 +81,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
-type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
+type rawnum = NumTok.Signed.t
 
 (** The unique id string below will be used to refer to a particular
     registered interpreter/uninterpreter of numeral or string notation.
@@ -116,8 +116,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of string
-  | Abstract of string
+  | Warning of NumTok.UnsignedNat.t
+  | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
   { uint : Names.inductive;
diff --git a/interp/numTok.ml b/interp/numTok.ml
index c11acdc8bd..e254e9e972 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -8,55 +8,243 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type t = {
-  int : string;
-  frac : string;
-  exp : string
-}
-
-let equal n1 n2 =
-  String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
-
-let int s = { int = s; frac = ""; exp = "" }
-
-let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
-
-let parse =
-  let buff = ref (Bytes.create 80) in
-  let store len x =
-    let open Bytes in
-    if len >= length !buff then
-      buff := cat !buff (create (length !buff));
-    set !buff len x;
-    succ len in
-  let get_buff len = Bytes.sub_string !buff 0 len in
-  (* reads [0-9_]* *)
-  let rec number len s = match Stream.peek s with
-    | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s
-    | _ -> len in
-  fun s ->
-  let i = get_buff (number 0 s) in
-  let f =
-    match Stream.npeek 2 s with
-    | '.' :: (('0'..'9' | '_') as c) :: _ ->
-       Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
-    | _ -> "" in
-  let e =
-    match (Stream.npeek 2 s) with
-    | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
-       Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
-    | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
-       begin match Stream.npeek 3 s with
-       | _ :: _ :: ('0'..'9' as c) :: _ ->
-          Stream.junk s; Stream.junk s; Stream.junk s;
-          get_buff (number (store (store (store 0 e) sign) c) s)
-       | _ -> ""
-       end
-    | _ -> "" in
-  { int = i; frac = f; exp = e }
-
-let of_string s =
-  if s = "" || s.[0] < '0' || s.[0] > '9' then None else
-    let strm = Stream.of_string (s ^ "  ") in
-    let n = parse strm in
-    if Stream.count strm >= String.length s then Some n else None
+(** We keep the string to preserve the user representation,
+    e.g. "e"/"E" or the presence of leading 0s, or the presence of a +
+    in the exponent *)
+
+module UnsignedNat =
+struct
+  type t = string
+  let of_string s =
+    assert (String.length s > 0);
+    assert (s.[0] >= '0' && s.[0] <= '9');
+    s
+  let to_string s =
+    String.(concat "" (split_on_char '_' s))
+
+  let sprint s = s
+  let print s = Pp.str (sprint s)
+
+  (** Comparing two raw numbers (base 10, big-endian, non-negative).
+      A bit nasty, but not critical: used e.g. to decide when a number
+      is considered as large (see threshold warnings in notation.ml). *)
+
+  exception Comp of int
+
+  let rec compare s s' =
+    let l = String.length s and l' = String.length s' in
+    if l < l' then - compare s' s
+    else
+      let d = l-l' in
+      try
+        for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
+        for i = d to l-1 do
+          let c = Util.pervasives_compare s.[i] s'.[i-d] in
+          if c != 0 then raise (Comp c)
+        done;
+        0
+      with Comp c -> c
+
+   let is_zero s =
+     compare s "0" = 0
+end
+
+type sign = SPlus | SMinus
+
+module SignedNat =
+struct
+  type t = sign * UnsignedNat.t
+  let of_string s =
+    assert (String.length s > 0);
+    let sign,n =
+      match s.[0] with
+      | '-' -> (SMinus,String.sub s 1 (String.length s - 1))
+      | '+' -> (SPlus,String.sub s 1 (String.length s - 1))
+      | _ -> (SPlus,s) in
+    (sign,UnsignedNat.of_string n)
+  let to_string (sign,n) =
+    (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
+  let to_bigint n = Bigint.of_string (to_string n)
+  let of_bigint n =
+    let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+    (sign, Bigint.to_string n)
+end
+
+module Unsigned =
+struct
+
+  type t = {
+    int : string;  (** \[0-9\]\[0-9_\]* *)
+    frac : string;  (** empty or \[0-9_\]+ *)
+    exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+  }
+
+  let equal n1 n2 =
+    String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
+
+  let parse =
+    let buff = ref (Bytes.create 80) in
+    let store len x =
+      let open Bytes in
+      if len >= length !buff then
+        buff := cat !buff (create (length !buff));
+      set !buff len x;
+      succ len in
+    let get_buff len = Bytes.sub_string !buff 0 len in
+    (* reads [0-9_]* *)
+    let rec number len s = match Stream.peek s with
+      | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
+      | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
+      | _ -> len in
+    fun s ->
+    let i = get_buff (number 0 s) in
+    assert (i <> "");
+    let f =
+      match Stream.npeek 2 s with
+      | '.' :: (('0'..'9' | '_') as c) :: _ ->
+         Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
+      | _ -> "" in
+    let e =
+      match (Stream.npeek 2 s) with
+      | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+         Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
+      | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+         begin match Stream.npeek 3 s with
+         | _ :: _ :: ('0'..'9' as c) :: _ ->
+            Stream.junk s; Stream.junk s; Stream.junk s;
+            get_buff (number (store (store (store 0 e) sign) c) s)
+         | _ -> ""
+         end
+      | _ -> "" in
+    { int = i; frac = f; exp = e }
+
+  let sprint n =
+    n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
+
+  let print n =
+    Pp.str (sprint n)
+
+  let parse_string s =
+    if s = "" || s.[0] < '0' || s.[0] > '9' then None else
+      let strm = Stream.of_string (s ^ "  ") in
+      let n = parse strm in
+      if Stream.count strm >= String.length s then Some n else None
+
+  let of_string s =
+    match parse_string s with
+    | None -> assert false
+    | Some s -> s
+
+  let to_string =
+    sprint (* We could remove the '_' but not necessary for float_of_string *)
+
+  let to_nat = function
+    | { int = i; frac = ""; exp = "" } -> Some i
+    | _ -> None
+
+  let is_nat = function
+    | { int = _; frac = ""; exp = "" } -> true
+    | _ -> false
+
+end
+
+open Unsigned
+
+module Signed =
+struct
+
+  type t = sign * Unsigned.t
+
+  let equal (s1,n1) (s2,n2) =
+    s1 = s2 && equal n1 n2
+
+  let is_zero = function
+    | (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac
+    | _ -> false
+
+  let of_decimal_and_exponent (sign,int) f e =
+    let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in
+    let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in
+    sign, { int; frac; exp }
+
+  let to_decimal_and_exponent (sign, { int; frac; exp }) =
+    let e =
+      if exp = "" then None else
+        Some (match exp.[1] with
+        | '-' -> SMinus, String.sub exp 2 (String.length exp - 2)
+        | '+' -> SPlus, String.sub exp 2 (String.length exp - 2)
+        | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in
+    let f = if frac = "" then None else Some frac in
+    (sign, int), f, e
+
+  let of_nat i =
+    (SPlus,{ int = i; frac = ""; exp = "" })
+
+  let of_int (s,i) =
+    (s,{ int = i; frac = ""; exp = "" })
+
+  let of_int_string s = of_int (SignedNat.of_string s)
+
+  let to_int = function
+    | (s, { int = i; frac = ""; exp = "" }) -> Some (s,i)
+    | _ -> None
+
+  let is_int n = match to_int n with None -> false | Some _ -> true
+
+  let sprint (s,i) =
+    (match s with SPlus -> "" | SMinus -> "-") ^ Unsigned.sprint i
+
+  let print i =
+    Pp.str (sprint i)
+
+  let parse_string s =
+    if s = "" || s = "-" || s = "+" ||
+       (s.[0] < '0' || s.[0] > '9') && ((s.[0] <> '-' && s.[0] <> '+') || s.[1] < '0' || s.[1] > '9') then None else
+      let strm = Stream.of_string (s ^ "  ") in
+      let sign = match s.[0] with
+        | '-' -> (Stream.junk strm; SMinus)
+        | '+' -> (Stream.junk strm; SPlus)
+        | _ -> SPlus in
+      let n = parse strm in
+      if Stream.count strm >= String.length s then Some (sign,n) else None
+
+  let of_string s =
+    assert (s <> "");
+    let sign,u = match s.[0] with
+    | '-' -> (SMinus, String.sub s 1 (String.length s - 1))
+    | '+' -> (SPlus, String.sub s 1 (String.length s - 1))
+    | _ -> (SPlus, s) in
+    (sign, Unsigned.of_string u)
+
+  let to_string (sign,u) =
+    (match sign with SPlus -> "" | SMinus -> "-") ^ Unsigned.to_string u
+
+  let to_bigint = function
+    | (sign, { int = n; frac = ""; exp = "" }) ->
+      Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n))
+    | _ -> None
+
+  let of_bigint n =
+    let sign, int = SignedNat.of_bigint n in
+    (sign, { int; frac = ""; exp = "" })
+
+  let to_bigint_and_exponent (s, { int; frac; exp }) =
+    let s = match s with SPlus -> "" | SMinus -> "-" in
+    let int = UnsignedNat.to_string int in
+    let frac = UnsignedNat.to_string frac in
+    let i = Bigint.of_string (s ^ int ^ frac) in
+    let e =
+      let e = if exp = "" then Bigint.zero else match exp.[1] with
+      | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))
+      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))))
+      | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in
+      Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in
+    (i,e)
+
+  let of_bigint_and_exponent i e =
+    of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e))
+
+  let is_bigger_int_than (s, { int; frac; exp }) i =
+    frac = "" && exp = "" && UnsignedNat.compare int i >= 0
+
+end
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 141f1be889..ea289df237 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -8,21 +8,125 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type t = {
-  int : string;  (** \[0-9\]\[0-9_\]* *)
-  frac : string;  (** empty or \[0-9_\]+ *)
-  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
-}
+(** Numerals in different forms: signed or unsigned, possibly with
+    fractional part and exponent.
 
-val equal : t -> t -> bool
+    Numerals are represented using raw strings of decimal
+    literals and a separate sign flag.
 
-(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *)
-val int : string -> t
+    Note that this representation is not unique, due to possible
+    multiple leading or trailing zeros, and -0 = +0, for instances.
+    The reason to keep the numeral exactly as it was parsed is that
+    specific notations can be declared for specific numerals
+    (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
+    [Notation "2e1" := ...]). Those notations override the generic
+    interpretation as numeral. So, one has to record the form of the
+    numeral which exactly matches the notation. *)
 
-val to_string : t -> string
+type sign = SPlus | SMinus
 
-val of_string : string -> t option
+(** {6 String representation of a natural number } *)
 
-(** Precondition: the first char on the stream is a digit (\[0-9\]).
-    Precondition: at least two extra chars after the numeral to parse. *)
-val parse : char Stream.t -> t
+module UnsignedNat :
+sig
+  type t
+  val of_string : string -> t
+    (** Convert from a non-empty sequence of digits (which may contain "_") *)
+
+  val to_string : t -> string
+    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val compare : t -> t -> int
+end
+
+(** {6 String representation of a signed natural number } *)
+
+module SignedNat :
+sig
+  type t = sign * UnsignedNat.t
+  val of_string : string -> t
+    (** Convert from a non-empty sequence of digits which may contain "_" *)
+
+  val to_string : t -> string
+    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+
+  val to_bigint : t -> Bigint.bigint
+  val of_bigint : Bigint.bigint -> t
+end
+
+(** {6 Unsigned decimal numerals } *)
+
+module Unsigned :
+sig
+  type t
+  val equal : t -> t -> bool
+  val is_nat : t -> bool
+  val to_nat : t -> string option
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val parse : char Stream.t -> t
+    (** Parse a positive Coq numeral.
+        Precondition: the first char on the stream is already known to be a digit (\[0-9\]).
+        Precondition: at least two extra chars after the numeral to parse.
+
+        The recognized syntax is:
+        - integer part: \[0-9\]\[0-9_\]*
+        - decimal part: empty or .\[0-9_\]+
+        - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+
+  val parse_string : string -> t option
+    (** Parse the string as a positive Coq numeral, if possible *)
+
+end
+
+(** {6 Signed decimal numerals } *)
+
+module Signed :
+sig
+  type t = sign * Unsigned.t
+  val equal : t -> t -> bool
+  val is_zero : t -> bool
+  val of_nat : UnsignedNat.t -> t
+  val of_int : SignedNat.t -> t
+  val to_int : t -> SignedNat.t option
+  val is_int : t -> bool
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val parse_string : string -> t option
+    (** Parse the string as a signed Coq numeral, if possible *)
+
+  val of_int_string : string -> t
+    (** Convert from a string in the syntax of OCaml's int/int64 *)
+
+  val of_string : string -> t
+    (** Convert from a string in the syntax of OCaml's string_of_float *)
+
+  val to_string : t -> string
+    (** Returns a string in the syntax of OCaml's float_of_string *)
+
+  val of_bigint : Bigint.bigint -> t
+  val to_bigint : t -> Bigint.bigint option
+    (** Convert from and to bigint when the denotation of a bigint *)
+
+  val of_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
+  val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
+    (** n, p and q such that the number is n.p*10^q *)
+
+  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint
+  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t
+    (** n and p such that the number is n*10^p *)
+
+  val is_bigger_int_than : t -> UnsignedNat.t -> bool
+    (** Test if an integer whose absolute value is bounded *)
+
+end
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 6a436fbcb7..a39da96a53 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -723,7 +723,7 @@ let rec next_token ~diff_mode loc s =
         let ep = Stream.count s in
         IDENT id, set_loc_pos loc bp ep end
   | Some ('0'..'9') ->
-      let n = NumTok.parse s in
+      let n = NumTok.Unsigned.parse s in
       let ep = Stream.count s in
       comment_stop bp;
       (NUMERAL n, set_loc_pos loc bp ep)
@@ -813,7 +813,7 @@ let token_text : type c. c Tok.p -> string = function
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
   | PNUMERAL None -> "numeral"
-  | PNUMERAL (Some n) -> "'" ^ NumTok.to_string n ^ "'"
+  | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
   | PLEFTQMARK -> "LEFTQMARK"
@@ -888,6 +888,6 @@ let terminal s =
   else PKEYWORD s
 
 (* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-let terminal_numeral s = match NumTok.of_string s with
+let terminal_numeral s = match NumTok.Unsigned.parse_string s with
   | Some n -> PNUMERAL (Some n)
   | None -> failwith "numeral token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3ce6981879..2c1284c4db 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -50,7 +50,7 @@ val check_keyword : string -> unit
 val terminal : string -> string Tok.p
 
 (** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-val terminal_numeral : string -> NumTok.t Tok.p
+val terminal_numeral : string -> NumTok.Unsigned.t Tok.p
 
 (** The lexer of Coq: *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 3fd756e748..963f029766 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -174,7 +174,7 @@ GRAMMAR EXTEND Gram
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
-            | CPrim (Numeral (SPlus,n)) ->
+            | CPrim (Numeral (NumTok.SPlus,n)) ->
                 CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
@@ -248,7 +248,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id, None) }
@@ -355,12 +355,12 @@ GRAMMAR EXTEND Gram
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
-          | CPatPrim (Numeral (SPlus,n)) ->
+          | CPatPrim (Numeral (NumTok.SPlus,n)) ->
               CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   fixannot:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index e8e802f606..9c50109bb3 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -21,15 +21,18 @@ let _ = List.iter CLexer.add_keyword prim_kw
 
 let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
 
-let check_int loc = function
-  | { NumTok.int = i; frac = ""; exp = "" } -> i
-  | _ -> CErrors.user_err ~loc (Pp.str "This number is not an integer.")
-
-let my_int_of_string loc s =
+let my_int_of_string ?loc s =
   try
     int_of_string s
   with Failure _ ->
-    CErrors.user_err ~loc (Pp.str "This number is too large.")
+    CErrors.user_err ?loc (Pp.str "This number is too large.")
+
+let my_to_nat_string ?loc ispos s =
+  match NumTok.Unsigned.to_nat s with
+  | Some n -> n
+  | None ->
+    let pos = if ispos then "a natural" else "an integer" in
+    CErrors.user_err ?loc Pp.(str "This number is not " ++ str pos ++ str " number.")
 
 let test_pipe_closedcurly =
   let open Pcoq.Lookahead in
@@ -47,7 +50,7 @@ let test_minus_nat =
 
 GRAMMAR EXTEND Gram
   GLOBAL:
-    bigint natural integer identref name ident var preident
+    bignat bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string lstring pattern_ident pattern_identref by_notation
     smart_global bar_cbrace;
@@ -122,15 +125,18 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
-      | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
+    [ [ i = bigint -> { my_int_of_string ~loc i } ] ]
   ;
   natural:
-    [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
+    [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
   ;
-  bigint: (* Negative numbers are dealt with elsewhere *)
-    [ [ i = NUMERAL -> { check_int loc i } ] ]
+  bigint:
+    [ [ i = NUMERAL -> { my_to_nat_string true ~loc i }
+      | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ]
   ;
+  bignat:
+    [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ]
+ ;
   bar_cbrace:
     [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe2412fcd7..b3f997e1b3 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -166,7 +166,7 @@ struct
   | _ -> None
 
   let lk_nat tok n strm = match stream_nth n strm with
-  | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+  | Tok.NUMERAL p when NumTok.Unsigned.is_nat p -> Some (n + 1)
   | _ -> None
 
   let rec lk_list lk_elem n strm =
@@ -462,6 +462,7 @@ module Prim =
     let ident = gec_gen "ident"
     let natural = gec_gen "natural"
     let integer = gec_gen "integer"
+    let bignat = Entry.create "Prim.bignat"
     let bigint = Entry.create "Prim.bigint"
     let string = gec_gen "string"
     let lstring = Entry.create "Prim.lstring"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cd97ea20fa..87c7f168ce 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -171,6 +171,7 @@ module Prim :
     val pattern_ident : Id.t Entry.t
     val pattern_identref : lident Entry.t
     val base_ident : Id.t Entry.t
+    val bignat : string Entry.t
     val natural : int Entry.t
     val bigint : string Entry.t
     val integer : int Entry.t
diff --git a/parsing/tok.ml b/parsing/tok.ml
index ff4433f18c..b1ceab8822 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,7 +17,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.t option -> NumTok.t p
+  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -31,7 +31,7 @@ let pattern_strings : type c. c p -> string * string option =
   | PIDENT s -> "IDENT", s
   | PFIELD s -> "FIELD", s
   | PNUMERAL None -> "NUMERAL", None
-  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.to_string n)
+  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.Unsigned.sprint n)
   | PSTRING s -> "STRING", s
   | PLEFTQMARK -> "LEFTQMARK", None
   | PBULLET s -> "BULLET", s
@@ -43,7 +43,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.t
+  | NUMERAL of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -59,7 +59,7 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
   | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
   | PNUMERAL None, PNUMERAL None -> Some Util.Refl
-  | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.equal n1 n2 -> Some Util.Refl
+  | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl
   | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
   | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
   | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
@@ -73,7 +73,7 @@ let equal t1 t2 = match t1, t2 with
 | PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
 | IDENT s1, IDENT s2 -> string_equal s1 s2
 | FIELD s1, FIELD s2 -> string_equal s1 s2
-| NUMERAL n1, NUMERAL n2 -> NumTok.equal n1 n2
+| NUMERAL n1, NUMERAL n2 -> NumTok.Unsigned.equal n1 n2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -100,7 +100,7 @@ let extract_string diff_mode = function
     else s
   | PATTERNIDENT s -> s
   | FIELD s -> if diff_mode then "." ^ s else s
-  | NUMERAL n -> NumTok.to_string n
+  | NUMERAL n -> NumTok.Unsigned.sprint n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -124,7 +124,7 @@ let match_pattern (type c) (p : c p) : t -> c =
   let err () = raise Stream.Failure in
   let seq = string_equal in
   match p with
-  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.to_string n) -> s | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
   | PIDENT None -> (function IDENT s' -> s' | _ -> err ())
   | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
   | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())
@@ -132,7 +132,7 @@ let match_pattern (type c) (p : c p) : t -> c =
   | PFIELD None -> (function FIELD s -> s | _ -> err ())
   | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
   | PNUMERAL None -> (function NUMERAL s -> s | _ -> err ())
-  | PNUMERAL (Some n) -> let s = NumTok.to_string n in (function NUMERAL n' when s = NumTok.to_string n' -> n' | _ -> err ())
+  | PNUMERAL (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMERAL n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ())
   | PSTRING None -> (function STRING s -> s | _ -> err ())
   | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
   | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 6d0691a746..b556194eb3 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,7 +15,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.t option -> NumTok.t p
+  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -29,7 +29,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.t
+  | NUMERAL of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5bfbe7a49a..5a26ac8827 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -125,7 +125,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | _ -> ElimOnConstr clbind
 
 let mkNumeral n =
-  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
+  Numeral (NumTok.Signed.of_int_string (string_of_int n))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 1dca8fd57b..442b40221b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -350,8 +350,8 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) ->
-             let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
+          | _, Constrexpr.Numeral n when NumTok.Signed.is_int n ->
+            int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
         | None -> raise Not_found
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 23d4d63228..dadce9a9ea 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -22,9 +22,8 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 (*** Parsing for float in digital notation ***)
 
-let interp_float ?loc (sign,n) =
-  let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in
-  DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n)))
+let interp_float ?loc n =
+  DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n)))
 
 (* Pretty printing is already handled in constrextern.ml *)
 
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..e66dbe17b2 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -21,16 +21,16 @@ open Pcoq.Prim
 
 let pr_numnot_option = function
   | Nop -> mt ()
-  | Warning n -> str "(warning after " ++ str n ++ str ")"
-  | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+  | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
+  | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
 
 }
 
 VERNAC ARGUMENT EXTEND numnotoption
   PRINTED BY { pr_numnot_option }
 | [ ] -> { Nop }
-| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 7043653f7b..e0dc3d8989 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Glob_term
 open Bigint
-open Constrexpr
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -113,8 +112,8 @@ let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
 
 let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
 
-let r_of_rawnum ?loc (sign,n) =
-  let n, f, e = NumTok.(n.int, n.frac, n.exp) in
+let r_of_rawnum ?loc n =
+  let n,e = NumTok.Signed.to_bigint_and_exponent n in
   let izr z =
     DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
   let rmult r r' =
@@ -126,15 +125,7 @@ let r_of_rawnum ?loc (sign,n) =
     let e = pos_of_bignat e in
     DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in
   let n =
-    let n = Bigint.of_string (n ^ f) in
-    let n = match sign with SPlus -> n | SMinus -> Bigint.(neg n) in
     izr (z_of_int ?loc n) in
-  let e =
-    let e = if e = "" then Bigint.zero else match e.[1] with
-      | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
-      | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
-      | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
-    Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in
   if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
   else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
   else n  (* e = 0 *)
@@ -146,9 +137,7 @@ let r_of_rawnum ?loc (sign,n) =
 let rawnum_of_r c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_IZR ->
      let n = bigint_of_z a in
-     let s, n =
-       if is_strictly_neg n then SMinus, neg n else SPlus, n in
-     s, NumTok.int (to_string n)
+     NumTok.Signed.of_bigint n
   | GApp (md,  [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
      begin match DAst.get l, DAst.get r with
      | GApp (i, [l]), GApp (i', [r])
@@ -161,11 +150,8 @@ let rawnum_of_r c = match DAst.get c with
            else
              let i = bigint_of_z l in
              let e = bignat_of_pos e in
-             let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in
-             let i = Bigint.to_string i in
-             let se = if is_gr md glob_Rdiv then "-" else "" in
-             let e = "e" ^ se ^ Bigint.to_string e in
-             s, { NumTok.int = i; frac = ""; exp = e }
+             let e = if is_gr md glob_Rdiv then neg e else e in
+             NumTok.Signed.of_bigint_and_exponent i e
         | _ -> raise Non_closed_number
         end
      | _ -> raise Non_closed_number
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 21b9cd4f1f..b285c0abcc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -77,8 +77,8 @@ let tag_var = tag Tag.variable
     | LevelSome -> true
 
   let prec_of_prim_token = function
-    | Numeral (SPlus,_) -> lposint
-    | Numeral (SMinus,_) -> lnegint
+    | Numeral (NumTok.SPlus,_) -> lposint
+    | Numeral (NumTok.SMinus,_) -> lnegint
     | String _ -> latom
 
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -222,8 +222,7 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral (SPlus,n) -> str (NumTok.to_string n)
-    | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n)
+    | Numeral n -> NumTok.Signed.print n
     | String s -> qs s
 
   let pr_evar pr id l =
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6696f1431e..0d8a6ebed7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -417,14 +417,16 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  output=$*.out.real; \
+	  export LC_CTYPE=C; \
+	  export LANG=C; \
 	  $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
-	    | grep -v "Welcome to Coq" \
-	    | grep -v "\[Loading ML file" \
-	    | grep -v "Skipping rcfile loading" \
-	    | grep -v "^<W>" \
+	    | grep -a -v "Welcome to Coq" \
+	    | grep -a -v "\[Loading ML file" \
+	    | grep -a -v "Skipping rcfile loading" \
+	    | grep -a -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$output; \
-	  diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
+	  diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 113384e9cf..060877707b 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -218,3 +218,19 @@ let v : ty := Build_ty Set set in v : ty
      : ty
 let v : ty := Build_ty Type type in v : ty
      : ty
+1
+     : nat
+(-1000)%Z
+     : Z
+0
+     : Prop
++0
+     : bool
+-0
+     : bool
+00
+     : nat * nat
+1000
+     : Prop
+1_000
+     : list nat
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 22aff36d67..47e1b127cb 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -457,3 +457,33 @@ Module Test20.
   Check let v := 4%kt in v : ty.
   Check let v := 5%kt in v : ty.
 End Test20.
+
+Module Test21.
+
+  Check 00001.
+  Check (-1_000)%Z.
+
+End Test21.
+
+Module Test22.
+
+Notation "0" := False.
+Notation "+0" := true.
+Notation "-0" := false.
+Notation "00" := (0%nat, 0%nat).
+Check 0.
+Check +0.
+Check -0.
+Check 00.
+
+Notation "1000" := True.
+Notation "1_000" := (cons 1 nil).
+Check 1000.
+Check 1_000.
+
+(* To do: preserve parsing of -0:
+Require Import ZArith.
+Check (-0)%Z.
+*)
+
+End Test22.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 2b14ca7069..ebc272d9af 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -4,6 +4,8 @@
      : R
 15e-1%R
      : R
+15%R
+     : R
 eq_refl : 102e-2 = 102e-2
      : 102e-2 = 102e-2
 eq_refl : 102e-1 = 102e-1
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 7be8b18ac8..e5f9d06316 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -3,6 +3,7 @@ Check 32%R.
 Check (-31)%R.
 
 Check 1.5_%R.
+Check 1_.5_e1_%R.
 
 Open Scope R_scope.
 
diff --git a/test-suite/output/allBytes.out b/test-suite/output/allBytes.out
new file mode 100644
index 0000000000..8d188c4c45
--- /dev/null
+++ b/test-suite/output/allBytes.out
@@ -0,0 +1 @@
+!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~
diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v
new file mode 100644
index 0000000000..01a5161ef4
--- /dev/null
+++ b/test-suite/output/allBytes.v
@@ -0,0 +1,121 @@
+(* Taken from bedrock2 *)
+
+(* Note: not an utf8 file *)
+
+Require Import Coq.ZArith.BinInt Coq.Lists.List.
+Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String.
+
+Definition allBytes: list Byte.byte :=
+  map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with
+                 | Some b => b
+                 | None => Byte.x00 (* won't happen *)
+                 end)
+      (seq 32 95).
+
+Notation "a b" := (@cons Byte.byte a b)
+  (only printing, right associativity, at level 3, format "a b").
+
+Notation "" := (@nil Byte.byte)
+  (only printing, right associativity, at level 3, format "").
+
+Notation "  " := (Byte.x20) (only printing).
+Notation "'!'" := (Byte.x21) (only printing).
+Notation "'""'" := (Byte.x22) (only printing).
+Notation "'#'" := (Byte.x23) (only printing).
+Notation "'$'" := (Byte.x24) (only printing).
+Notation "'%'" := (Byte.x25) (only printing).
+Notation "'&'" := (Byte.x26) (only printing).
+Notation "'''" := (Byte.x27) (only printing).
+Notation "'('" := (Byte.x28) (only printing).
+Notation "')'" := (Byte.x29) (only printing).
+Notation "'*'" := (Byte.x2a) (only printing).
+Notation "'+'" := (Byte.x2b) (only printing).
+Notation "','" := (Byte.x2c) (only printing).
+Notation "'-'" := (Byte.x2d) (only printing).
+Notation "'.'" := (Byte.x2e) (only printing).
+Notation "'/'" := (Byte.x2f) (only printing).
+Notation "'0'" := (Byte.x30) (only printing).
+Notation "'1'" := (Byte.x31) (only printing).
+Notation "'2'" := (Byte.x32) (only printing).
+Notation "'3'" := (Byte.x33) (only printing).
+Notation "'4'" := (Byte.x34) (only printing).
+Notation "'5'" := (Byte.x35) (only printing).
+Notation "'6'" := (Byte.x36) (only printing).
+Notation "'7'" := (Byte.x37) (only printing).
+Notation "'8'" := (Byte.x38) (only printing).
+Notation "'9'" := (Byte.x39) (only printing).
+Notation "':'" := (Byte.x3a) (only printing).
+Notation "';'" := (Byte.x3b) (only printing).
+Notation "'<'" := (Byte.x3c) (only printing).
+Notation "'='" := (Byte.x3d) (only printing).
+Notation "'>'" := (Byte.x3e) (only printing).
+Notation "'?'" := (Byte.x3f) (only printing).
+Notation "'@'" := (Byte.x40) (only printing).
+Notation "'A'" := (Byte.x41) (only printing).
+Notation "'B'" := (Byte.x42) (only printing).
+Notation "'C'" := (Byte.x43) (only printing).
+Notation "'D'" := (Byte.x44) (only printing).
+Notation "'E'" := (Byte.x45) (only printing).
+Notation "'F'" := (Byte.x46) (only printing).
+Notation "'G'" := (Byte.x47) (only printing).
+Notation "'H'" := (Byte.x48) (only printing).
+Notation "'I'" := (Byte.x49) (only printing).
+Notation "'J'" := (Byte.x4a) (only printing).
+Notation "'K'" := (Byte.x4b) (only printing).
+Notation "'L'" := (Byte.x4c) (only printing).
+Notation "'M'" := (Byte.x4d) (only printing).
+Notation "'N'" := (Byte.x4e) (only printing).
+Notation "'O'" := (Byte.x4f) (only printing).
+Notation "'P'" := (Byte.x50) (only printing).
+Notation "'Q'" := (Byte.x51) (only printing).
+Notation "'R'" := (Byte.x52) (only printing).
+Notation "'S'" := (Byte.x53) (only printing).
+Notation "'T'" := (Byte.x54) (only printing).
+Notation "'U'" := (Byte.x55) (only printing).
+Notation "'V'" := (Byte.x56) (only printing).
+Notation "'W'" := (Byte.x57) (only printing).
+Notation "'X'" := (Byte.x58) (only printing).
+Notation "'Y'" := (Byte.x59) (only printing).
+Notation "'Z'" := (Byte.x5a) (only printing).
+Notation "'['" := (Byte.x5b) (only printing).
+Notation "'\'" := (Byte.x5c) (only printing).
+Notation "']'" := (Byte.x5d) (only printing).
+Notation "'^'" := (Byte.x5e) (only printing).
+Notation "'_'" := (Byte.x5f) (only printing).
+Notation "'`'" := (Byte.x60) (only printing).
+Notation "'a'" := (Byte.x61) (only printing).
+Notation "'b'" := (Byte.x62) (only printing).
+Notation "'c'" := (Byte.x63) (only printing).
+Notation "'d'" := (Byte.x64) (only printing).
+Notation "'e'" := (Byte.x65) (only printing).
+Notation "'f'" := (Byte.x66) (only printing).
+Notation "'g'" := (Byte.x67) (only printing).
+Notation "'h'" := (Byte.x68) (only printing).
+Notation "'i'" := (Byte.x69) (only printing).
+Notation "'j'" := (Byte.x6a) (only printing).
+Notation "'k'" := (Byte.x6b) (only printing).
+Notation "'l'" := (Byte.x6c) (only printing).
+Notation "'m'" := (Byte.x6d) (only printing).
+Notation "'n'" := (Byte.x6e) (only printing).
+Notation "'o'" := (Byte.x6f) (only printing).
+Notation "'p'" := (Byte.x70) (only printing).
+Notation "'q'" := (Byte.x71) (only printing).
+Notation "'r'" := (Byte.x72) (only printing).
+Notation "'s'" := (Byte.x73) (only printing).
+Notation "'t'" := (Byte.x74) (only printing).
+Notation "'u'" := (Byte.x75) (only printing).
+Notation "'v'" := (Byte.x76) (only printing).
+Notation "'w'" := (Byte.x77) (only printing).
+Notation "'x'" := (Byte.x78) (only printing).
+Notation "'y'" := (Byte.x79) (only printing).
+Notation "'z'" := (Byte.x7a) (only printing).
+Notation "'{'" := (Byte.x7b) (only printing).
+Notation "'|'" := (Byte.x7c) (only printing).
+Notation "'}'" := (Byte.x7d) (only printing).
+Notation "'~'" := (Byte.x7e) (only printing).
+
+Global Set Printing Width 300.
+
+Goal False.
+  let cc := eval cbv in allBytes in idtac cc.
+Abort.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1d790e7cd2..5dae389a62 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
 | TTName -> MayRecNo (Aentry Prim.name)
 | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
-| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTBigint -> MayRecNo (Aentry Prim.bignat)
 | TTReference -> MayRecNo (Aentry Constr.global)
 
 let interp_entry forpat e = match e with
@@ -411,8 +411,8 @@ match e with
 | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
   begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v)))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v)))
   end
 | TTReference ->
   begin match forpat with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 22e4e35ad4..475d5c31f7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -252,7 +252,7 @@ let quote_notation_token x =
 let is_numeral symbs =
   match List.filter (function Break _ -> false | _ -> true) symbs with
   | ([Terminal "-"; Terminal x] | [Terminal x]) ->
-      NumTok.of_string x <> None
+      NumTok.Unsigned.parse_string x <> None
   | _ ->
       false