diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f6943871c..0c7dbeeb0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -215,7 +215,9 @@ GEXTEND Gram | IDENT "Parameters" -> (Global, Definitional) ] ] ; inline: - [ ["Inline" -> true | -> false] ] + [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) + | IDENT "Inline" -> Some (Flags.get_inline_level()) + | -> None] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) @@ -443,12 +445,14 @@ GEXTEND Gram | -> [] ] ] ; module_expr_inl: - [ [ "!"; me = module_expr -> (me,false) - | me = module_expr -> (me,true) ] ] + [ [ "!"; me = module_expr -> (me,None) + | "<"; i = INT; ">"; me = module_expr -> (me,Some (int_of_string i)) + | me = module_expr -> (me,Some (Flags.get_inline_level())) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> (me,false) - | me = module_type -> (me,true) ] ] + [ [ "!"; me = module_type -> (me,None) + | "<"; i = INT; ">"; me = module_type -> (me,Some (int_of_string i)) + | me = module_type -> (me,Some (Flags.get_inline_level())) ] ] ; (* Module binder *) module_binder: |