diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 10 |
2 files changed, 12 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3bc27965ab..3a99b24738 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -413,8 +413,13 @@ GEXTEND Gram VernacRequireFrom (export, None, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr)) - | IDENT "Include"; "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ] + | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr)) + | IDENT "Include"; "Type"; expr = module_type -> + VernacInclude(false,CIMTE(expr)) + | IDENT "Include"; "Self"; expr = module_expr -> + VernacInclude(true,CIME(expr)) + | IDENT "Include"; "Self"; "Type"; expr = module_type -> + VernacInclude(true,CIMTE(expr)) ] ] ; export_token: [ [ IDENT "Import" -> Some false diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 9e7bd10e74..52ef1875f4 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -761,15 +761,15 @@ let rec pr_vernac = function let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Module Type " ++ pr_lident id ++ b ++ pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) - | VernacInclude (in_ast) -> + | VernacInclude (b,in_ast) -> begin match in_ast with | CIMTE mty -> - hov 2 (str"Include" ++ - (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty) + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + pr_module_type pr_lconstr mty) | CIME mexpr -> - hov 2 (str"Include" ++ - (fun me -> str " " ++ pr_module_expr me) mexpr) + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + pr_module_expr mexpr) end (* Solving *) | VernacSolve (i,tac,deftac) -> |