diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
| commit | be6f3a6234ee809dd3c290621d80c3280a41355e (patch) | |
| tree | 8fed697f726193b765c8a2faeedd34ad60b541cb /vernac | |
| parent | 2e1aa5c15ad524cffd03c7979992af44ab2bb715 (diff) | |
| parent | 6af420bb384af0acf94028fc44ef44fd5a6fd841 (diff) | |
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
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 6 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 9 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
3 files changed, 8 insertions, 9 deletions
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 |