Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.

25 files changed, 307 insertions, 120 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index fce4db1869..26e1e25fb9 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -225,7 +225,8 @@ function
 | "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
 | "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
 | "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
-| "NUMERAL", s -> fprintf fmt "Tok.PNUMERAL (%a)" print_pat s
+| "NUMERAL", None -> fprintf fmt "Tok.PNUMERAL None"
+| "NUMERAL", Some s -> fprintf fmt "Tok.PNUMERAL (Some (NumTok.int %a))" print_string s
 | "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
 | "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
 | "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
@@ -463,7 +464,10 @@ end =
 struct
 
 let terminal s =
-  let c = Printf.sprintf "Extend.Atoken (CLexer.terminal \"%s\")" s in
+  let p =
+    if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral"
+    else "CLexer.terminal" in
+  let c = Printf.sprintf "Extend.Atoken (%s \"%s\")" p s in
   SymbQuote c
 
 let rec parse_symb self = function
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index fa19eb8ec4..7a14a4e708 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -48,13 +48,23 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
-(** Representation of integer literals that appear in Coq scripts.
-    We now use raw strings of digits in base 10 (big-endian), and a separate
-    sign flag. Note that this representation is not unique, due to possible
-    multiple leading zeros, and -0 = +0 *)
+(** 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 = string
+type raw_numeral = NumTok.t
 
 type prim_token =
   | Numeral of sign * raw_numeral
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 338ffb706d..60610b92b8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -50,8 +50,8 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-(* Note: redundant Numeral representations such as -0 and +0 (or different
-   numbers of leading zeros) are considered different here. *)
+(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+   are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
 | Numeral (SPlus,n1), Numeral (SPlus,n2)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4866ff3db5..24b1362e6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -318,16 +318,11 @@ 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_number s =
-  let rec aux i =
-    Int.equal (String.length s) i ||
-    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
-  in aux 0
-
 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
@@ -337,10 +332,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
         mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
 	match decompose_notation_key ntn, l with
-        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
-           mkprim (loc, Numeral (SMinus,x))
-        | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
-           mkprim (loc, Numeral (SPlus,x))
+        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+           begin match NumTok.of_string x with
+           | Some n -> mkprim (loc, Numeral (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))
+           | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
 let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
@@ -969,7 +968,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
   | GInt i ->
-     CPrim(Numeral (SPlus, Uint63.to_string i))
+     CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
 
   in insert_coercion coercion (CAst.make ?loc c)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 86fcf7fd56..8b93088515 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1489,6 +1489,7 @@ 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 merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 147eaf20dc..1262dbb181 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+NumTok
 Constrexpr
 Tactypes
 Stdarg
diff --git a/interp/notation.ml b/interp/notation.ml
index 6cb95db364..df8f6eb4f8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -506,9 +506,11 @@ module InnerPrimToken = struct
   let do_interp ?loc interp primtok =
     match primtok, interp with
     | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n)
-    | Numeral (s,n), BigNumInterp interp -> interp ?loc (ofNumeral s n)
+    | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }),
+      BigNumInterp interp -> interp ?loc (ofNumeral s n)
     | String s, StringInterp interp -> interp ?loc s
-    | _ -> raise Not_found
+    | (Numeral _ | String _),
+      (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
 
   type uninterpreter =
     | RawNumUninterp of (any_glob_constr -> rawnum option)
@@ -522,8 +524,10 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    if Bigint.is_pos_or_zero n then Numeral (SPlus,Bigint.to_string n)
-    else Numeral (SMinus,Bigint.to_string (Bigint.neg 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)))
 
   let mkString = function
     | None -> None
@@ -560,8 +564,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_numeral
-  | Abstract of raw_numeral
+  | Warning of string
+  | Abstract of string
 
 type int_ty =
   { uint : Names.inductive;
@@ -571,11 +575,16 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
+type decimal_ty =
+  { int : int_ty;
+    decimal : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
 
 type string_target_kind =
   | ListByte
@@ -767,11 +776,24 @@ let coquint_of_rawnum uint str =
   in
   do_chars str (String.length str - 1) nil
 
-let coqint_of_rawnum inds (sign,str) =
+let coqint_of_rawnum inds sign str =
   let uint = coquint_of_rawnum inds.uint str 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 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
+    mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|])  (* DecimalExp *)
+
 let rawnum_of_coquint c =
   let rec of_uint_loop c buf =
     match Constr.kind c with
@@ -790,7 +812,7 @@ 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 Buffer.contents buf
+  else NumTok.int (Buffer.contents buf)
 
 let rawnum_of_coqint c =
   match Constr.kind c with
@@ -801,6 +823,19 @@ let rawnum_of_coqint 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
+  match Constr.kind c with
+  | App (_,[|i; f|]) -> of_ife i f None
+  | App (_,[|i; f; e|]) -> of_ife i f (Some e)
+  | _ -> raise NotAValidPrimToken
 
 (***********************************************************************)
 
@@ -887,32 +922,42 @@ let bigint_of_int63 c =
   | _ -> raise NotAValidPrimToken
 
 let big2raw n =
-  if Bigint.is_pos_or_zero n then (SPlus, Bigint.to_string n)
-  else (SMinus, Bigint.to_string (Bigint.neg 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
+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, n) when rawnum_compare n threshold >= 0 ->
+  | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" })
+       when rawnum_compare n threshold >= 0 ->
      warn_large_num o.ty_name
   | _ -> ()
   end;
-  let c = match fst o.to_kind with
-    | Int int_ty -> coqint_of_rawnum int_ty n
-    | UInt uint_ty when fst n == SPlus -> coquint_of_rawnum uint_ty (snd n)
-    | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
-    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
-    | Int63 -> interp_int63 ?loc (raw2big n)
+  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)
+    | (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
   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) threshold >= 0 ->
+  | Abstract threshold, Direct
+       when rawnum_compare (snd n).NumTok.int threshold >= 0 ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
      glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
@@ -928,6 +973,7 @@ let uninterp o n =
       | (UInt _, c) -> (SPlus, rawnum_of_coquint c)
       | (Z _, c) -> big2raw (bigint_of_z c)
       | (Int63, c) -> big2raw (bigint_of_int63 c)
+      | (Decimal _, c) -> rawnum_of_decimal c
     end o n
 end
 
@@ -1252,8 +1298,8 @@ let find_notation ntn sc =
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, n
-  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^n
+  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
+  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string 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 5423655229..57e2be16b9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -70,10 +70,10 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
-(** A numeral interpreter is the pair of an interpreter for **integer**
+(** A numeral interpreter is the pair of an interpreter for **decimal**
    numbers in terms and an optional interpreter in pattern, if
-   negative numbers are not supported, the interpreter must fail with
-   an appropriate error message *)
+   non integer or negative numbers are not supported, the interpreter
+   must fail with an appropriate error message *)
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
@@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_numeral
-  | Abstract of raw_numeral
+  | Warning of string
+  | Abstract of string
 
 type int_ty =
   { uint : Names.inductive;
@@ -123,11 +123,16 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
+type decimal_ty =
+  { int : int_ty;
+    decimal : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
 
 type string_target_kind =
   | ListByte
diff --git a/interp/numTok.ml b/interp/numTok.ml
new file mode 100644
index 0000000000..cdc6ddb62b
--- /dev/null
+++ b/interp/numTok.ml
@@ -0,0 +1,52 @@
+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
diff --git a/interp/numTok.mli b/interp/numTok.mli
new file mode 100644
index 0000000000..46223c5faf
--- /dev/null
+++ b/interp/numTok.mli
@@ -0,0 +1,18 @@
+type t = {
+  int : string;  (** \[0-9\]+ *)
+  frac : string;  (** empty or \[0-9\]+ *)
+  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]+ *)
+}
+
+val equal : t -> t -> bool
+
+(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *)
+val int : string -> t
+
+val to_string : t -> string
+
+val of_string : string -> t option
+
+(** 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
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index f2e51afff5..42ca5f8c05 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -318,10 +318,6 @@ let rec ident_tail loc len s = match Stream.peek s with
           warn_unrecognized_unicode ~loc (u,id); len
       | _ -> len
 
-let rec number len s = match Stream.peek s with
-  | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
-  | _ -> len
-
 let warn_comment_terminator_in_string =
   CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
          (fun () ->
@@ -706,15 +702,11 @@ let rec next_token ~diff_mode loc s =
       let id = get_buff len in
       comment_stop bp;
       (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
-  | Some ('0'..'9' as c) ->
-      Stream.junk s;
-      let len =
-        try number (store 0 c) s with
-          Stream.Failure -> raise (Stream.Error "")
-      in
+  | Some ('0'..'9') ->
+      let n = NumTok.parse s in
       let ep = Stream.count s in
       comment_stop bp;
-      (NUMERAL (get_buff len), set_loc_pos loc bp ep)
+      (NUMERAL n, set_loc_pos loc bp ep)
   | Some '\"' ->
       Stream.junk s;
       let (loc, len) =
@@ -796,8 +788,8 @@ let token_text : type c. c Tok.p -> string = function
   | PKEYWORD t -> "'" ^ t ^ "'"
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
-  | PNUMERAL None -> "integer"
-  | PNUMERAL (Some s) -> "'" ^ s ^ "'"
+  | PNUMERAL None -> "numeral"
+  | PNUMERAL (Some n) -> "'" ^ NumTok.to_string n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
   | PLEFTQMARK -> "LEFTQMARK"
@@ -846,12 +838,6 @@ module LexerDiff = MakeLexer (struct let mode = true end)
 let is_ident_not_keyword s =
   is_ident s && not (is_keyword s)
 
-let is_number s =
-  let rec aux i =
-    Int.equal (String.length s) i ||
-    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
-  in aux 0
-
 let strip s =
   let len =
     let rec loop i len =
@@ -875,5 +861,9 @@ let terminal s =
   let s = strip s in
   let () = match s with "" -> failwith "empty token." | _ -> () in
   if is_ident_not_keyword s then PIDENT (Some s)
-  else if is_number s then PNUMERAL (Some s)
   else PKEYWORD s
+
+(* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
+let terminal_numeral s = match NumTok.of_string s with
+  | Some n -> PNUMERAL (Some n)
+  | None -> failwith "numeral token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 9df3e45f49..464bcf614d 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -46,9 +46,12 @@ val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
 
-(** When string is neither an ident nor an int, returns a keyword. *)
+(** When string is not an ident, returns a keyword. *)
 val terminal : string -> string Tok.p
 
+(** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
+val terminal_numeral : string -> NumTok.t Tok.p
+
 (** The lexer of Coq: *)
 
 module Lexer :
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 9c5fe2a71d..80dd997860 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -21,6 +21,10 @@ 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 =
   try
     int_of_string s
@@ -110,13 +114,13 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = NUMERAL      -> { my_int_of_string loc i }
-      | "-"; i = NUMERAL -> { - my_int_of_string loc i } ] ]
+    [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
+      | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
   ;
   natural:
-    [ [ i = NUMERAL -> { my_int_of_string loc i } ] ]
+    [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
   ;
   bigint: (* Negative numbers are dealt with elsewhere *)
-    [ [ i = NUMERAL -> { i } ] ]
+    [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b733ff46d4..5d8897cb47 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -157,7 +157,7 @@ module Prim :
     val pattern_identref : lident Entry.t
     val base_ident : Id.t Entry.t
     val natural : int Entry.t
-    val bigint : Constrexpr.raw_numeral Entry.t
+    val bigint : string Entry.t
     val integer : int Entry.t
     val string : string Entry.t
     val lstring : lstring Entry.t
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 36d319d543..71e2d4aa80 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 : string option -> string p
+  | PNUMERAL : NumTok.t option -> NumTok.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -30,7 +30,8 @@ let pattern_strings : type c. c p -> string * string option =
   | PPATTERNIDENT s -> "PATTERNIDENT", s
   | PIDENT s -> "IDENT", s
   | PFIELD s -> "FIELD", s
-  | PNUMERAL s -> "INT", s
+  | PNUMERAL None -> "NUMERAL", None
+  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.to_string n)
   | PSTRING s -> "STRING", s
   | PLEFTQMARK -> "LEFTQMARK", None
   | PBULLET s -> "BULLET", s
@@ -42,7 +43,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of string
+  | NUMERAL of NumTok.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -57,7 +58,8 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
   | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
-  | PNUMERAL s1, PNUMERAL 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
   | 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
@@ -71,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 s1, NUMERAL s2 -> string_equal s1 s2
+| NUMERAL n1, NUMERAL n2 -> NumTok.equal n1 n2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -98,7 +100,7 @@ let extract_string diff_mode = function
     else s
   | PATTERNIDENT s -> s
   | FIELD s -> if diff_mode then "." ^ s else s
-  | NUMERAL s -> s
+  | NUMERAL n -> NumTok.to_string n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -122,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' | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.to_string 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 ())
@@ -130,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 s) -> (function NUMERAL s' when seq s s' -> s' | _ -> err ())
+  | PNUMERAL (Some n) -> let s = NumTok.to_string n in (function NUMERAL n' when s = NumTok.to_string 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 2b3bb85174..a5fb5ad9cd 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 : string option -> string p
+  | PNUMERAL : NumTok.t option -> NumTok.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 string
+  | NUMERAL of NumTok.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 90dda4850e..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -148,7 +148,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),string_of_int (abs n))
+  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs 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 457b333a16..7cd62f4ead 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -360,7 +360,7 @@ 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,s) ->
+          | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) ->
              let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
           | _ -> raise Not_found
           end
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 525056e5f1..ec8c2338fb 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -56,17 +56,24 @@ let locate_z () =
     }, mkRefC q_z)
   else None
 
-let locate_int () =
+let locate_decimal () =
   let int = "num.int.type" in
   let uint = "num.uint.type" in
-  if Coqlib.has_ref int && Coqlib.has_ref uint
+  let dec = "num.decimal.type" in
+  if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec
   then
     let q_int = qualid_of_ref int in
     let q_uint = qualid_of_ref uint in
-    Some ({
+    let q_dec = qualid_of_ref dec in
+    let int_ty = {
         int = unsafe_locate_ind q_int;
         uint = unsafe_locate_ind q_uint;
-    }, mkRefC q_int, mkRefC q_uint)
+      } in
+    let dec_ty = {
+        int = int_ty;
+        decimal = unsafe_locate_ind q_dec;
+      } in
+    Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec)
   else None
 
 let locate_int63 () =
@@ -86,16 +93,16 @@ let type_error_to f ty =
   CErrors.user_err
     (pr_qualid f ++ str " should go from Decimal.int to " ++
      pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let type_error_of g ty =
   CErrors.user_err
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
-     str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+     str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let vernac_numeral_notation env sigma local ty f g scope opts =
-  let int_ty = locate_int () in
+  let dec_ty = locate_decimal () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -110,11 +117,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
   let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
-    match int_ty with
-    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    match dec_ty with
+    | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+    | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -127,11 +136,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
   in
   (* Check the type of g *)
   let of_kind =
-    match int_ty with
-    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    match dec_ty with
+    | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+    | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1c496efb8f..0ae3de7321 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -235,8 +235,8 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral (SPlus,n) -> str n
-    | Numeral (SMinus,n) -> str ("-"^n)
+    | Numeral (SPlus,n) -> str (NumTok.to_string n)
+    | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n)
     | String s -> qs s
 
   let pr_evar pr id l =
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index b0ac9ea29f..4cd0ffb1dc 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -19,30 +19,31 @@ Nat.div2: nat -> nat
 Nat.log2: nat -> nat
 Nat.succ: nat -> nat
 Nat.sqrt: nat -> nat
+S: nat -> nat
 Nat.pred: nat -> nat
 Nat.double: nat -> nat
 Nat.square: nat -> nat
-S: nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
 Nat.tail_mul: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.of_uint: Decimal.uint -> nat
+Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 Nat.div2: nat -> nat
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 3d4b3d0568..1a7dadb2c3 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -16,6 +16,8 @@
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
+Require Import Datatypes.
+
 (** Unsigned integers are just lists of digits.
     For instance, ten is (D1 (D0 Nil)) *)
 
@@ -42,6 +44,15 @@ Notation zero := (D0 Nil).
 
 Variant int := Pos (d:uint) | Neg (d:uint).
 
+(** For decimal numbers, we use two constructors [Decimal] and
+    [DecimalExp], depending on whether or not they are given with an
+    exponent (e.g., 1.02e+01). [i] is the integral part while [f] is
+    the fractional part (beware that leading zeroes do matter). *)
+
+Variant decimal :=
+ | Decimal (i:int) (f:uint)
+ | DecimalExp (i:int) (f:uint) (e:int).
+
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
@@ -52,6 +63,14 @@ Bind Scope dec_int_scope with int.
 
 Register uint as num.uint.type.
 Register int as num.int.type.
+Register decimal as num.decimal.type.
+
+Fixpoint nb_digits d :=
+  match d with
+  | Nil => O
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d =>
+    S (nb_digits d)
+  end.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
@@ -115,6 +134,28 @@ Fixpoint revapp (d d' : uint) :=
 
 Definition rev d := revapp d Nil.
 
+Definition app d d' := revapp (rev d) d'.
+
+Definition app_int d1 d2 :=
+  match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end.
+
+(** [nztail] removes all trailing zero digits and return both the
+    result and the number of removed digits. *)
+
+Definition nztail d :=
+  let fix aux d_rev :=
+    match d_rev with
+    | D0 d_rev => let (r, n) := aux d_rev in pair r (S n)
+    | _ => pair d_rev O
+    end in
+  let (r, n) := aux (rev d) in pair (rev r) n.
+
+Definition nztail_int d :=
+  match d with
+  | Pos d => let (r, n) := nztail d in pair (Pos r) n
+  | Neg d => let (r, n) := nztail d in pair (Neg r) n
+  end.
+
 Module Little.
 
 (** Successor of little-endian numbers *)
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 01e59bbed6..568e5b9997 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -245,7 +245,7 @@ type prod_info = production_level * production_position
 type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
-| TTBigint : ('self, Constrexpr.raw_numeral) entry
+| TTBigint : ('self, string) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -403,8 +403,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,v)))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,v)))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
   end
 | TTReference ->
   begin match forpat with
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d80f29cf1b..1e6a928c7c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
   ;
   inline:
-    [ [ IDENT "Inline"; "("; i = NUMERAL; ")" -> { InlineAt (int_of_string i) }
+    [ [ IDENT "Inline"; "("; i = natural; ")" -> { InlineAt i }
       | IDENT "Inline" -> { DefaultInline }
       | -> { NoInline } ] ]
   ;
@@ -607,8 +607,8 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   functor_app_annot:
-    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = NUMERAL; "]" ->
-        { InlineAt (int_of_string i) }
+    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = natural; "]" ->
+        { InlineAt i }
       | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline }
       | -> { DefaultInline }
       ] ]
@@ -847,8 +847,7 @@ GRAMMAR EXTEND Gram
   strategy_level:
     [ [ IDENT "expand" -> { Conv_oracle.Expand }
       | IDENT "opaque" -> { Conv_oracle.Opaque }
-      | n=NUMERAL -> { Conv_oracle.Level (int_of_string n) }
-      | "-"; n=NUMERAL -> { Conv_oracle.Level (- int_of_string n) }
+      | n=integer -> { Conv_oracle.Level n }
       | IDENT "transparent" -> { Conv_oracle.transparent } ] ]
   ;
   instance_name:
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index b5e9e1b0d5..843296d24e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -250,7 +250,7 @@ let quote_notation_token x =
 let is_numeral symbs =
   match List.filter (function Break _ -> false | _ -> true) symbs with
   | ([Terminal "-"; Terminal x] | [Terminal x]) ->
-      (try let _ = Bigint.of_string x in true with Failure _ -> false)
+      NumTok.of_string x <> None
   | _ ->
       false