From 2a31e23df8ff0ab67a09008858fa49e77e5f4332 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jan 2020 01:04:07 +0100
Subject: Adding bignat to parse positive numbers; bigint now includes negative
 ints.

Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.
---
 parsing/g_prim.mlg           | 13 ++++++++-----
 parsing/pcoq.ml              |  1 +
 parsing/pcoq.mli             |  1 +
 plugins/syntax/g_numeral.mlg |  4 ++--
 vernac/egramcoq.ml           |  2 +-
 5 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index e8e802f606..2bc1c11596 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -47,7 +47,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,13 +122,16 @@ 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 *)
+  bigint:
+    [ [ i = NUMERAL -> { check_int loc i }
+      | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ]
+  ;
+  bignat:
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe2412fcd7..fccd096d11 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -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/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..eccefdf64a 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -29,8 +29,8 @@ let pr_numnot_option = function
 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 waft }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract n }
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1d790e7cd2..6f8ee76b33 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
-- 
cgit v1.2.3


From 08189431706298d599cffea2e41dd51290305ba3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jan 2020 13:36:34 +0100
Subject: Centralizing all kinds of numeral string management in numTok.ml.

Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent

In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.

Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
---
 dev/doc/changes.md                     |   2 +
 dev/top_printers.dbg                   |   2 +
 dev/top_printers.ml                    |   2 +
 dev/top_printers.mli                   |   2 +
 interp/constrexpr.ml                   |  20 +--
 interp/constrexpr_ops.ml               |   5 +-
 interp/constrextern.ml                 |  29 ++--
 interp/constrintern.ml                 |  11 +-
 interp/notation.ml                     | 140 ++++++----------
 interp/notation.mli                    |   6 +-
 interp/numTok.ml                       | 287 +++++++++++++++++++++++++++------
 interp/numTok.mli                      | 130 +++++++++++++--
 parsing/cLexer.ml                      |   6 +-
 parsing/cLexer.mli                     |   2 +-
 parsing/g_constr.mlg                   |   8 +-
 parsing/g_prim.mlg                     |  27 ++--
 parsing/pcoq.ml                        |   2 +-
 parsing/tok.ml                         |  16 +-
 parsing/tok.mli                        |   4 +-
 plugins/ltac/g_tactic.mlg              |   2 +-
 plugins/ssr/ssrparser.mlg              |   4 +-
 plugins/syntax/float_syntax.ml         |   5 +-
 plugins/syntax/g_numeral.mlg           |   8 +-
 plugins/syntax/r_syntax.ml             |  24 +--
 printing/ppconstr.ml                   |   7 +-
 test-suite/output/NumeralNotations.out |   4 +
 test-suite/output/NumeralNotations.v   |   7 +
 test-suite/output/RealSyntax.out       |   2 +
 test-suite/output/RealSyntax.v         |   1 +
 vernac/egramcoq.ml                     |   4 +-
 vernac/metasyntax.ml                   |   2 +-
 31 files changed, 496 insertions(+), 275 deletions(-)

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..0d0f17f358 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -8,55 +8,238 @@
 (*         *     (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] <> '-');
+    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 n =
+    let sign,n =
+      if String.length n > 0 && n.[0] = '-'
+      then (SMinus,String.sub n 1 (String.length n - 1))
+      else (SPlus,n) in
+    (sign,UnsignedNat.of_string n)
+  let to_string (s,n) =
+    (match s with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
+  let to_bigint s = Bigint.of_string (to_string s)
+  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.[0] < '0' || s.[0] > '9') && (s.[0] <> '-' || s.[1] < '0' || s.[1] > '9') then None else
+      let strm = Stream.of_string (s ^ "  ") in
+      let sign = if s.[0] = '-' then (Stream.junk strm; SMinus) else 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 2bc1c11596..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
@@ -122,18 +125,18 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = bigint -> { my_int_of_string loc i } ] ]
+    [ [ i = bigint -> { my_int_of_string ~loc i } ] ]
   ;
   natural:
-    [ [ i = bignat -> { my_int_of_string loc i } ] ]
+    [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
   ;
   bigint:
-    [ [ i = NUMERAL -> { check_int loc i }
-      | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ]
+    [ [ i = NUMERAL -> { my_to_nat_string true ~loc i }
+      | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ]
   ;
   bignat:
-    [ [ i = NUMERAL -> { check_int loc i } ] ]
-  ;
+    [ [ 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 fccd096d11..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 =
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 eccefdf64a..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" bignat(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bignat(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/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 113384e9cf..bb299eff97 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -218,3 +218,7 @@ 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
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 22aff36d67..31154d9f45 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -457,3 +457,10 @@ 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.
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/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 6f8ee76b33..5dae389a62 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -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
 
-- 
cgit v1.2.3


From 475650c6425fb3ed91f388db7e7da918950f0194 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Feb 2020 11:41:04 +0100
Subject: Test-suite: Assume coqtop output is text even with non-printable
 characters.

---
 test-suite/Makefile | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

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"; \
-- 
cgit v1.2.3


From b0d34aa8cb8b0b84d6749312553d5d03709cf5f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Feb 2020 11:09:57 +0100
Subject: Adding a test for printing single characters.

Originally from bedrock2.
---
 test-suite/output/allBytes.out |   1 +
 test-suite/output/allBytes.v   | 121 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 122 insertions(+)
 create mode 100644 test-suite/output/allBytes.out
 create mode 100644 test-suite/output/allBytes.v

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.
-- 
cgit v1.2.3


From 8b8a612940127084d0162408eda5a1fe77365e79 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Feb 2020 05:14:18 +0100
Subject: Overlay for QuickChick

---
 .../11703-herbelin-master+turning-numTok-into-a-numeral-API.sh      | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh

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
-- 
cgit v1.2.3


From f7687371270e0b3fd3b61db3f25128c567aa7033 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 Mar 2020 21:09:22 +0100
Subject: Adding support for parsing "+" sig in NumTok.

Support in the parser needs yet to be added though.
---
 interp/numTok.ml | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

diff --git a/interp/numTok.ml b/interp/numTok.ml
index 0d0f17f358..e254e9e972 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -17,7 +17,7 @@ struct
   type t = string
   let of_string s =
     assert (String.length s > 0);
-    assert (s.[0] <> '-');
+    assert (s.[0] >= '0' && s.[0] <= '9');
     s
   let to_string s =
     String.(concat "" (split_on_char '_' s))
@@ -54,15 +54,17 @@ type sign = SPlus | SMinus
 module SignedNat =
 struct
   type t = sign * UnsignedNat.t
-  let of_string n =
+  let of_string s =
+    assert (String.length s > 0);
     let sign,n =
-      if String.length n > 0 && n.[0] = '-'
-      then (SMinus,String.sub n 1 (String.length n - 1))
-      else (SPlus,n) in
+      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 (s,n) =
-    (match s with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
-  let to_bigint s = Bigint.of_string (to_string s)
+  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)
@@ -196,10 +198,13 @@ struct
     Pp.str (sprint i)
 
   let parse_string s =
-    if s = "" || s = "-" ||
-       (s.[0] < '0' || s.[0] > '9') && (s.[0] <> '-' || s.[1] < '0' || s.[1] > '9') then None else
+    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 = if s.[0] = '-' then (Stream.junk strm; SMinus) else SPlus 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
 
-- 
cgit v1.2.3


From 5d1c4ae7b8931c7a1dec5f61c2571919319aeb4a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 17 Mar 2020 13:00:21 +0100
Subject: Testing notations which are specific numerals.

---
 test-suite/output/NumeralNotations.out | 12 ++++++++++++
 test-suite/output/NumeralNotations.v   | 23 +++++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index bb299eff97..060877707b 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -222,3 +222,15 @@ let v : ty := Build_ty Type type in v : ty
      : 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 31154d9f45..47e1b127cb 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -464,3 +464,26 @@ Module Test21.
   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.
-- 
cgit v1.2.3