diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 589b15fd41..d80f29cf1b 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 = INT; ")" -> { InlineAt (int_of_string i) } + [ [ IDENT "Inline"; "("; i = NUMERAL; ")" -> { InlineAt (int_of_string i) } | IDENT "Inline" -> { DefaultInline } | -> { NoInline } ] ] ; @@ -607,7 +607,7 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; functor_app_annot: - [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = NUMERAL; "]" -> { InlineAt (int_of_string i) } | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline } | -> { DefaultInline } @@ -847,8 +847,8 @@ 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=NUMERAL -> { Conv_oracle.Level (int_of_string n) } + | "-"; n=NUMERAL -> { Conv_oracle.Level (- int_of_string n) } | IDENT "transparent" -> { Conv_oracle.transparent } ] ] ; instance_name: |