diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 37 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 25 |
2 files changed, 35 insertions, 27 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3a99b24738..38ab689f55 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -389,13 +389,13 @@ GEXTEND Gram [ [ (* Interactive module declaration *) IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; mty_o = OPT of_module_type; - mexpr_o = OPT is_module_expr -> - VernacDefineModule (export, id, bl, mty_o, mexpr_o) - + o = OPT is_module_expr -> + VernacDefineModule (export, id, bl, mty_o, + match o with None -> [] | Some l -> l) | IDENT "Module"; "Type"; id = identref; - bl = LIST0 module_binder; mty_o = OPT is_module_type -> - VernacDeclareModuleType (id, bl, mty_o) - + bl = LIST0 module_binder; o = OPT is_module_type -> + VernacDeclareModuleType (id, bl, + match o with None -> [] | Some l -> l) | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; ":"; mty = module_type -> VernacDeclareModule (export, id, bl, (mty,true)) @@ -413,28 +413,35 @@ 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(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)) ] ] + | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> + VernacInclude(false,CIME(e,l)) + | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type -> + VernacInclude(false,CIMTE(e,l)) + | IDENT "Include"; "Self"; e = module_expr -> + VernacInclude(true,CIME(e,[])) + | IDENT "Include"; "Self"; "Type"; e = module_type -> + VernacInclude(true,CIMTE(e,[])) ] ] ; export_token: [ [ IDENT "Import" -> Some false | IDENT "Export" -> Some true | -> None ] ] ; + ext_module_type: + [ [ "<+"; mty = module_type -> mty ] ] + ; + ext_module_expr: + [ [ "<+"; mexpr = module_expr -> mexpr ] ] + ; of_module_type: [ [ ":"; mty = module_type -> (mty, true) | "<:"; mty = module_type -> (mty, false) ] ] ; is_module_type: - [ [ ":="; mty = module_type -> mty ] ] + [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ] ; is_module_expr: - [ [ ":="; mexpr = module_expr -> mexpr ] ] + [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ] ; (* Module binder *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 52ef1875f4..4407ca6aa4 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -751,7 +751,8 @@ let rec pr_vernac = function hov 2 (str"Module" ++ spc() ++ pr_require_token export ++ pr_lident m ++ b ++ pr_opt (pr_of_module_type pr_lconstr) ty ++ - pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) + (if bd = [] then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd) | VernacDeclareModule (export,id,bl,m1) -> let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ @@ -760,17 +761,17 @@ let rec pr_vernac = function | VernacDeclareModuleType (id,bl,m) -> 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 (b,in_ast) -> - begin - match in_ast with - | CIMTE mty -> - hov 2 (str"Include " ++ str (if b then "Self " else "") ++ - pr_module_type pr_lconstr mty) - | CIME mexpr -> - hov 2 (str"Include " ++ str (if b then "Self " else "") ++ - pr_module_expr mexpr) - end + (if m = [] then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") + (pr_module_type pr_lconstr) m) + | VernacInclude (b,CIMTE(mty,mtys)) -> + let pr_mty = pr_module_type pr_lconstr in + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ str "Type " ++ + prlist_with_sep (fun () -> str " <+ ") pr_mty (mty::mtys)) + | VernacInclude (b,CIME(mexpr,mexprs)) -> + let pr_me = pr_module_expr in + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + prlist_with_sep (fun () -> str " <+ ") pr_me (mexpr::mexprs)) (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ |