diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 9 |
1 files changed, 4 insertions, 5 deletions
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: |