diff options
| author | letouzey | 2010-01-07 15:32:49 +0000 |
|---|---|---|
| committer | letouzey | 2010-01-07 15:32:49 +0000 |
| commit | 9b6517c0c933fb1d66c7feb53fa57e1697d8124a (patch) | |
| tree | d914d6bc2c5598baad03807ce40ada0b1d56045d /toplevel | |
| parent | e3e6ff629e258269bc9fe06f7be99a2d5f334071 (diff) | |
Include can accept both Module and Module Type
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 10 |
2 files changed, 10 insertions, 12 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7955d49163..b56b0b26fe 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -453,6 +453,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr + Modintern.interp_modexpr_or_modtype id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; @@ -493,6 +494,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr + Modintern.interp_modexpr_or_modtype id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef loc mp "mod"; @@ -540,6 +542,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_modtype + Modintern.interp_modexpr_or_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; if_verbose message @@ -550,13 +553,8 @@ let vernac_end_modtype (loc,id) = Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_include = function - | CIMTE mtys -> - Declaremods.declare_include - Modintern.interp_modtype mtys false - | CIME mexprs -> - Declaremods.declare_include - Modintern.interp_modexpr mexprs true +let vernac_include l = + Declaremods.declare_include Modintern.interp_modexpr_or_modtype l (**********************) (* Gallina extensions *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 2df396e095..d95fdbec95 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -176,7 +176,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder list * constr_expr option * constructor_expr list -type module_binder = bool option * lident list * module_type_ast +type module_binder = bool option * lident list * module_ast type grammar_tactic_prod_item_expr = | TacTerm of string @@ -264,12 +264,12 @@ type vernac_expr = (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * - module_binder list * module_type_ast + module_binder list * module_ast | VernacDefineModule of bool option * lident * - module_binder list * module_type_ast module_signature * module_ast list + module_binder list * module_ast module_signature * module_ast list | VernacDeclareModuleType of lident * - module_binder list * module_type_ast list * module_type_ast list - | VernacInclude of include_ast + module_binder list * module_ast list * module_ast list + | VernacInclude of module_ast list (* Solving *) |