diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 4 |
2 files changed, 11 insertions, 7 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: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 21281f6e4..42007e4b0 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -227,8 +227,8 @@ let rec pr_module_ast pr_c = function pr_module_ast pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") -let pr_module_ast_inl pr_c (mast,b) = - (if b then mt () else str "!") ++ pr_module_ast pr_c mast +let pr_module_ast_inl pr_c (mast,o) = + (if o=None then str "!" else mt ()) ++ pr_module_ast pr_c mast let pr_of_module_type prc = function | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty |