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.

3 files changed, 8 insertions, 9 deletions

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