Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01

36 files changed, 529 insertions, 183 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 1203ef6d18..ce8a787cd1 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -72,6 +72,14 @@ Notations
 - New command `String Notation` to register string syntax for custom
   inductive types.
 
+- Numeral notations now parse decimal constants such as 1.02e+01 or
+  10.2. Parsers added for Q and R. This should be considered as an
+  experimental feature currently.
+  Note: in -- the rare -- case when such numeral notations were used
+  in a development along with Q or R, they may have to be removed or
+  deconflicted through explicit scope annotations (1.23%Q,
+  45.6%R,...).
+
 - Various bugs have been fixed (e.g. PR #9214 on removing spurious
   parentheses on abbreviations shortening a strict prefix of an application).
 
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index baa6c2d64e..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
-| "INT", s -> fprintf fmt "Tok.PINT (%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/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
new file mode 100644
index 0000000000..67f6f8610a
--- /dev/null
+++ b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then
+
+    ltac2_CI_REF=master-parsing-decimal
+    ltac2_CI_GITURL=https://github.com/proux01/ltac2
+
+    quickchick_CI_REF=master-parsing-decimal
+    quickchick_CI_GITURL=https://github.com/proux01/QuickChick
+
+    Corn_CI_REF=master-parsing-decimal
+    Corn_CI_GITURL=https://github.com/proux01/corn
+
+    HoTT_CI_REF=master-parsing-decimal
+    HoTT_CI_GITURL=https://github.com/proux01/HoTT
+
+    stdlib2_CI_REF=master-parsing-decimal
+    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+fi
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8a5e9d87f8..5a1af9f9fa 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -74,14 +74,20 @@ Identifiers and access identifiers
   `.` (dot) without blank. They are used in the syntax of qualified
   identifiers.
 
-Natural numbers and integers
-  Numerals are sequences of digits. Integers are numerals optionally
-  preceded by a minus sign.
+Numerals
+  Numerals are sequences of digits with a potential fractional part
+  and exponent. Integers are numerals without fractional nor exponent
+  part and optionally preceded by a minus sign. Underscores ``_`` can
+  be used as comments in numerals.
 
   .. productionlist:: coq
      digit   : 0..9
      num     : `digit`…`digit`
      integer : [-]`num`
+     dot     : .
+     exp     : e | E
+     sign    : + | -
+     numeral : `num`[`dot` `num`][`exp`[`sign`]`num`]
 
 Strings
   Strings are delimited by ``"`` (double quote), and enclose a sequence of
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 7a5d07b2b7..63df3d37bf 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -943,8 +943,8 @@ instance the infix symbol ``+``, can be used to denote distinct
 definitions of the additive operator. Depending on which interpretation
 scopes are currently open, the interpretation is different.
 Interpretation scopes can include an interpretation for numerals and
-strings. However, this is only made possible at the Objective Caml
-level.
+strings, either at the OCaml level or using :cmd:`Numeral Notation`
+or :cmd:`String Notation`.
 
 .. cmd:: Declare Scope @scope
 
@@ -1214,7 +1214,7 @@ Scopes` or :cmd:`Print Scope`.
 
 ``nat_scope``
   This scope includes the standard arithmetical operators and relations on type
-  nat. Positive numerals in this scope are mapped to their canonical
+  nat. Positive integer numerals in this scope are mapped to their canonical
   representent built from :g:`O` and :g:`S`. The scope is delimited by the key
   ``nat``, and bound to the type :g:`nat` (see above).
 
@@ -1238,20 +1238,19 @@ Scopes` or :cmd:`Print Scope`.
   This scope includes the standard arithmetical operators and relations on
   type :g:`Q` (rational numbers defined as fractions of an integer and a
   strictly positive integer modulo the equality of the numerator-
-  denominator cross-product). As for numerals, only 0 and 1 have an
-  interpretation in scope ``Q_scope`` (their interpretations are 0/1 and 1/1
-  respectively).
+  denominator cross-product) and comes with an interpretation for numerals
+  as closed terms of type :g:`Q`.
 
 ``Qc_scope``
   This scope includes the standard arithmetical operators and relations on the
   type :g:`Qc` of rational numbers defined as the type of irreducible
   fractions of an integer and a strictly positive integer.
 
-``real_scope``
+``R_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes
   with an interpretation for numerals using the :g:`IZR` morphism from binary
-  integer numbers to :g:`R`.
+  integer numbers to :g:`R` and :g:`Z.pow_pos` for potential exponent parts.
 
 ``bool_scope``
   This scope includes notations for the boolean operators. It is delimited by the
@@ -1458,6 +1457,8 @@ Numeral notations
      * :n:`Decimal.uint -> option @ident__1`
      * :n:`Z -> @ident__1`
      * :n:`Z -> option @ident__1`
+     * :n:`Decimal.decimal -> @ident__1`
+     * :n:`Decimal.decimal -> option @ident__1`
 
    And the printing function :n:`@ident__3` should have one of the
    following types:
@@ -1468,6 +1469,8 @@ Numeral notations
      * :n:`@ident__1 -> option Decimal.uint`
      * :n:`@ident__1 -> Z`
      * :n:`@ident__1 -> option Z`
+     * :n:`@ident__1 -> Decimal.decimal`
+     * :n:`@ident__1 -> option Decimal.decimal`
 
      When parsing, the application of the parsing function
      :n:`@ident__2` to the number will be fully reduced, and universes
@@ -1501,15 +1504,16 @@ Numeral notations
      The numeral notation registered for :token:`type` does not support
      the given numeral.  This error is given when the interpretation
      function returns :g:`None`, or if the interpretation is registered
-     for only non-negative integers, and the given numeral is negative.
+     only for integers or non-negative integers, and the given numeral
+     has a fractional or exponent part or is negative.
 
 
-   .. exn:: @ident should go from Decimal.int to @type or (option @type). 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).
+   .. exn:: @ident should go from Decimal.int to @type or (option @type). 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).
 
      The parsing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
 
-   .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int).  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).
+   .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int).  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).
 
      The printing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 757d186c8b..7a14a4e708 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -48,16 +48,26 @@ 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 *)
-
-type sign = bool
-type raw_natural_number = string
+(** 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 raw_natural_number * sign
+  | Numeral of sign * raw_numeral
   | String of string
 
 type instance_expr = Glob_term.glob_level list
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 95a0039b0a..60610b92b8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -50,13 +50,14 @@ 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 (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2
+| Numeral (SPlus,n1), Numeral (SPlus,n2)
+| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2
 | String s1, String s2 -> String.equal s1 s2
-| _ -> false
+| (Numeral ((SPlus|SMinus),_) | 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 c2afa097bb..24b1362e6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -318,29 +318,28 @@ 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
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
+    | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) ->
         assert (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 (x,false))
-        | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
-	   mkprim (loc, Numeral (x,true))
+        | (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 (Uint63.to_string i,true))
+     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 7a3e9881ea..59feb46dc1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1487,8 +1487,9 @@ 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' && aux (i+1))
+    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
 
@@ -1513,11 +1514,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 (p, true)) } -> not (is_zero p)
+| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p)
 | _ -> false
 
 let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p)
+| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p)
 | _ -> false
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
@@ -1628,8 +1629,8 @@ let drop_notations_pattern looked_for genv =
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
-      let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
+      let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
       rcp_of_glob scopes pat
     | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
@@ -1944,8 +1945,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         GLetIn (na.CAst.v, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
-      let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
-       intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
+      let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
+       intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
     | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
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 2765661749..b9aca82cf4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -476,7 +476,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.raw_natural_number * Constrexpr.sign
+type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
 
 type prim_token_uid = string
 
@@ -499,15 +499,20 @@ module InnerPrimToken = struct
     | StringInterp f, StringInterp f' -> f == f'
     | _ -> false
 
-  let ofNumeral n s =
-    if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+  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 (n,s), RawNumInterp interp -> interp ?loc (n,s)
-    | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s)
+    | Numeral (s,n), RawNumInterp interp -> interp ?loc (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)
@@ -521,15 +526,17 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
-    else Numeral (Bigint.to_string (Bigint.neg n), false)
+    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
     | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
   let do_uninterp uninterp g = match uninterp with
-    | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g)
+    | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
     | BigNumUninterp u -> Option.map mkNumeral (u g)
     | StringUninterp u -> mkString (u g)
 
@@ -559,8 +566,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
+  | Warning of string
+  | Abstract of string
 
 type int_ty =
   { uint : Names.inductive;
@@ -570,11 +577,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
@@ -760,15 +772,29 @@ let coquint_of_rawnum uint str =
   let nil = mkConstruct (uint,1) in
   let rec do_chars s i acc =
     if i < 0 then acc
-    else
+    else if s.[i] == '_' then do_chars s (i-1) acc 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 (str,sign) =
+let coqint_of_rawnum inds sign str =
   let uint = coquint_of_rawnum inds.uint str in
-  mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
+  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 =
@@ -788,17 +814,30 @@ 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
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
-      | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
+      | 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
+  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
 
 (***********************************************************************)
 
@@ -885,31 +924,42 @@ let bigint_of_int63 c =
   | _ -> raise NotAValidPrimToken
 
 let big2raw n =
-  if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
-  else (Bigint.to_string (Bigint.neg n), false)
+  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 (n,s) =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string 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 with
-  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+  begin match o.warning, n with
+  | 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 snd n -> coquint_of_rawnum uint_ty (fst 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 (fst 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|]))
   | _ ->
@@ -922,9 +972,10 @@ let uninterp o n =
   PrimTokenNotation.uninterp
     begin function
       | (Int _, c) -> rawnum_of_coqint c
-      | (UInt _, c) -> (rawnum_of_coquint c, true)
+      | (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
 
@@ -1249,8 +1300,8 @@ let find_notation ntn sc =
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral (n,true) -> InConstrEntrySomeLevel, n
-  | Numeral (n,false) -> 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 5dcc96dc29..57e2be16b9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -70,14 +70,14 @@ 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
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
 
 (** The unique id string below will be used to refer to a particular
     registered interpreter/uninterpreter of numeral or string notation.
@@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
+  | 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..8f2004b889
--- /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..0b6a877cbd
--- /dev/null
+++ b/interp/numTok.mli
@@ -0,0 +1,18 @@
+type t = {
+  int : string;  (** \[0-9\]\[0-9_\]* *)
+  frac : string;  (** empty or \[0-9_\]+ *)
+  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[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 b81d89edf9..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;
-      (INT (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 ^ "'"
-  | PINT None -> "integer"
-  | PINT (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 PINT (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_constr.mlg b/parsing/g_constr.mlg
index 6f73a3e4ed..0586dda555 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -226,7 +226,7 @@ GRAMMAR EXTEND Gram
       | c=match_constr -> { c }
       | "("; c = operconstr LEVEL "200"; ")" ->
         { (match c.CAst.v with
-            | CPrim (Numeral (n,true)) ->
+            | CPrim (Numeral (SPlus,n)) ->
                 CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; "|}" -> { c }
@@ -305,7 +305,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) }
       | s=sort   -> { CAst.make ~loc @@  CSort s }
-      | n=INT    -> { CAst.make ~loc @@ CPrim (Numeral (n,true)) }
+      | n=NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (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) }
@@ -413,18 +413,18 @@ GRAMMAR EXTEND Gram
       | "_" -> { CAst.make ~loc @@ CPatAtom None }
       | "("; p = pattern LEVEL "200"; ")" ->
           { (match p.CAst.v with
-            | CPatPrim (Numeral (n,true)) ->
+            | CPatPrim (Numeral (SPlus,n)) ->
                  CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p) }
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           { let p =
             match p with
-            | { CAst.v = CPatPrim (Numeral (n,true)) } ->
+            | { CAst.v = CPatPrim (Numeral (SPlus,n)) } ->
                  CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc @@ CPatCast (p, ty) }
-      | n = INT    -> { CAst.make ~loc @@ CPatPrim (Numeral (n,true)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   impl_ident_tail:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 6247a12640..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 = INT      -> { my_int_of_string loc i }
-      | "-"; i = INT -> { - 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 = INT -> { 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 = INT -> { i } ] ]
+    [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e361f0d00f..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_natural_number 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 186d0502fc..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
-  | PINT : 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
-  | PINT 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
-  | INT 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
-  | PINT s1, PINT 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
-| INT s1, INT 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
-  | INT s -> s
+  | NUMERAL n -> NumTok.to_string n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -122,15 +124,15 @@ 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 ())
   | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ())
   | PFIELD None -> (function FIELD s -> s | _ -> err ())
   | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
-  | PINT None -> (function INT s -> s | _ -> err ())
-  | PINT (Some s) -> (function INT 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 ())
   | 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 678877720d..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
-  | PINT : 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
-  | INT 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 7bf705ffeb..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
-              | IDENT _ | INT _ ->
+              | IDENT _ | NUMERAL _ ->
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral 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/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 38bc58a659..e12bf36339 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -141,6 +141,11 @@ Ltac IZR_tac t :=
   match t with
   | R0 => constr:(0%Z)
   | R1 => constr:(1%Z)
+  | IZR (Z.pow_pos 10 ?p) =>
+    match isPcst p with
+    | true => constr:(Z.pow_pos 10 p)
+    | _ => constr:(InitialRing.NotConstant)
+    end
   | IZR ?u =>
     match isZcst u with
     | true => u
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..7cd62f4ead 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -224,20 +224,20 @@ let test_ssrslashnum b1 b2 strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "/" ->
       (match Util.stream_nth 1 strm with
-      | Tok.INT _ when b1 ->
+      | Tok.NUMERAL _ when b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
          | Tok.KEYWORD "/" ->
              if not b2 then () else begin
                match Util.stream_nth 3 strm with
-               | Tok.INT _ -> ()
+               | Tok.NUMERAL _ -> ()
                | _ -> raise Stream.Failure
              end
          | _ -> raise Stream.Failure)
       | Tok.KEYWORD "/" when not b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 3 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -248,7 +248,7 @@ let test_ssrslashnum b1 b2 strm =
   | Tok.KEYWORD "//" when not b1 ->
          (match Util.stream_nth 1 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 2 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -360,8 +360,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 (s,b) ->
-             let n = int_of_string s in if b then n else -n
+          | _, 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
         | None -> raise Not_found
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/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index d90b7d754c..b9062dd16b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -13,6 +13,7 @@ open Names
 open Globnames
 open Glob_term
 open Bigint
+open Constrexpr
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -104,22 +105,76 @@ let r_modpath = MPfile (make_dir rdefinitions)
 let r_path = make_path rdefinitions "R"
 
 let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-
-let r_of_int ?loc z =
-  DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
+
+let binintdef = ["Coq";"ZArith";"BinIntDef"]
+let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
+
+let glob_pow_pos = 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 izr z =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
+  let rmult r r' =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in
+  let rdiv r r' =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
+  let pow10 e =
+    let ten = z_of_int ?loc (Bigint.of_int 10) in
+    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 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 *)
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_r c = match DAst.get c with
+let rawnum_of_r c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_IZR ->
-      bigint_of_z a
+     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)
+  | 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])
+          when is_gr i glob_IZR && is_gr i' glob_IZR ->
+        begin match DAst.get r with
+        | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
+           let t = bigint_of_z t in
+           if not (Bigint.(equal t (of_int 10))) then
+             raise Non_closed_number
+           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 = se ^ Bigint.to_string e in
+             s, { NumTok.int = i; frac = ""; exp = e }
+        | _ -> raise Non_closed_number
+        end
+     | _ -> raise Non_closed_number
+     end
   | _ -> raise Non_closed_number
 
 let uninterp_r (AnyGlobConstr p) =
   try
-    Some (bigint_of_r p)
+    Some (rawnum_of_r p)
   with Non_closed_number ->
     None
 
@@ -131,11 +186,11 @@ let at_declare_ml_module f x =
 let r_scope = "R_scope"
 
 let _ =
-  register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+  register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r);
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
       pt_interp_info = Uid r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
-      pt_refs = [glob_IZR];
+      pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv];
       pt_in_match = false }
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 229930142e..0ae3de7321 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -84,7 +84,8 @@ let tag_var = tag Tag.variable
         | Any -> true
 
   let prec_of_prim_token = function
-    | Numeral (_,b) -> if b then lposint else lnegint
+    | Numeral (SPlus,_) -> lposint
+    | Numeral (SMinus,_) -> lnegint
     | String _ -> latom
 
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -234,7 +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 (n,s) -> str (if s then n else "-"^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/micromega/square.v b/test-suite/micromega/square.v
index 7266b662fa..9efb81a901 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -54,7 +54,7 @@ Qed.
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by
+ assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
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/test-suite/success/QArithSyntax.v b/test-suite/success/QArithSyntax.v
new file mode 100644
index 0000000000..2f2ee0134a
--- /dev/null
+++ b/test-suite/success/QArithSyntax.v
@@ -0,0 +1,9 @@
+Require Import QArith.
+Open Scope Q_scope.
+Check (eq_refl : 1.02 = 102 # 100).
+Check (eq_refl : 1.02e1 = 102 # 10).
+Check (eq_refl : 1.02e+03 = 1020).
+Check (eq_refl : 1.02e+02 = 102 # 1).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = -1 # 10000).
+Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v
new file mode 100644
index 0000000000..2765200991
--- /dev/null
+++ b/test-suite/success/RealSyntax.v
@@ -0,0 +1,19 @@
+Require Import Reals.
+Open Scope R_scope.
+Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
+Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+02 = IZR 102).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
+Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)).
+
+Goal 254e3 = 2540 * 10 ^ 2.
+ring.
+Qed.
+
+Require Import Psatz.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+lra.
+Qed.
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/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 139c4bf432..790bdf9ed6 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -29,12 +29,38 @@ Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.
 
 Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 
+Definition of_decimal (d:Decimal.decimal) : Q :=
+  let '(i, f, e) :=
+    match d with
+    | Decimal.Decimal i f => (i, f, Decimal.Pos Decimal.Nil)
+    | Decimal.DecimalExp i f e => (i, f, e)
+    end in
+  let num := Z.of_int (Decimal.app_int i f) in
+  let e := Z.sub (Z.of_int e) (Z.of_nat (Decimal.nb_digits f)) in
+  match e with
+  | Z0 => Qmake num 1
+  | Zpos e => Qmake (Pos.iter (Z.mul 10) num e) 1
+  | Zneg e => Qmake num (Pos.iter (Pos.mul 10) 1%positive e)
+  end.
+
+Definition to_decimal (q:Q) : option Decimal.decimal :=
+  let num := Z.to_int (Qnum q) in
+  let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
+  match den with
+  | Decimal.D1 Decimal.Nil =>
+    match Z.of_nat e_den with
+    | Z0 => Some (Decimal.Decimal num Decimal.Nil)
+    | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e)))
+    end
+  | _ => None
+  end.
+
+Numeral Notation Q of_decimal to_decimal : Q_scope.
+
 Definition inject_Z (x : Z) := Qmake x 1.
 Arguments inject_Z x%Z.
 
 Notation QDen p := (Zpos (Qden p)).
-Notation " 0 " := (0#1) : Q_scope.
-Notation " 1 " := (1#1) : Q_scope.
 
 Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
 Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index f1a08cc9b3..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_natural_number) 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 (v,true)))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true)))
+  | 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 2853d6e65f..e27f8b37b9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -293,7 +293,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
   ;
   inline:
-    [ [ IDENT "Inline"; "("; i = INT; ")" -> { InlineAt (int_of_string i) }
+    [ [ IDENT "Inline"; "("; i = natural; ")" -> { InlineAt i }
       | IDENT "Inline" -> { DefaultInline }
       | -> { NoInline } ] ]
   ;
@@ -606,8 +606,8 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   functor_app_annot:
-    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" ->
-        { InlineAt (int_of_string i) }
+    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = natural; "]" ->
+        { InlineAt i }
       | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline }
       | -> { DefaultInline }
       ] ]
@@ -846,8 +846,7 @@ GRAMMAR EXTEND Gram
   strategy_level:
     [ [ IDENT "expand" -> { Conv_oracle.Expand }
       | IDENT "opaque" -> { Conv_oracle.Opaque }
-      | n=INT -> { Conv_oracle.Level (int_of_string n) }
-      | "-"; n=INT -> { 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