diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c3d9438dea..5787186ad0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -222,9 +222,9 @@ GEXTEND Gram | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ] ; inline: - [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) - | IDENT "Inline" -> Some (Flags.get_inline_level()) - | -> None] ] + [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) + | IDENT "Inline" -> DefaultInline + | -> NoInline] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) |