diff options
| author | Pierre Roux | 2018-10-20 11:19:28 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:12 +0200 |
| commit | a95aacce6cc32726b494d4cc694da49eae86cf96 (patch) | |
| tree | 07caf6e22fd6ae991786cec51bf304ecd011bc02 /vernac | |
| parent | 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 (diff) | |
Rename the INT token to NUMERAL
In anticipation of future uses of this token for non integer numerals.
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: |