diff options
| author | letouzey | 2009-11-18 00:03:14 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-18 00:03:14 +0000 |
| commit | 2ddd0afea124874576b1468c3ce5830352be4322 (patch) | |
| tree | 5e49b6d68d695e89c861a13f860d76916c544051 /plugins/interface/xlate.ml | |
| parent | df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad (diff) | |
Module subtyping : allow many <: and module type declaration with <:
Any place where <: was legal can now contain many <: declarations.
Moreover we can say that the module type we are declaring is a subtype
of an earlier module type. See DecidableType2 for examples.
Also try to handle correctly the freeze/unfreeze summaries
when simulating start/include/end (syntax ... := ... <+ ...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/xlate.ml')
| -rw-r--r-- | plugins/interface/xlate.ml | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 97ab9efc88..9ba1d6715c 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1617,14 +1617,13 @@ let xlate_module_binder_list (l:module_binder list) = CT_module_binder (CT_id_ne_list(fst, idl2), xlate_module_type mty)) l);; -let xlate_module_type_check_opt = function - None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK - (CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE) - | Some(mty, true) -> CT_only_check(xlate_module_type mty) - | Some(mty, false) -> +let xlate_module_type_check = function + | Topconstr.Enforce mty -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK (CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT - (xlate_module_type mty));; + (xlate_module_type mty)) + | Topconstr.Check mtys -> + CT_only_check (List.map xlate_module_type mtys) let rec xlate_module_expr = function CMEident (_, qid) -> CT_coerce_ID_OPT_to_MODULE_EXPR @@ -2034,7 +2033,7 @@ let rec xlate_vernac = xlate_error"TODO: Local abbreviations and abbreviations with parameters" (* Modules and Module Types *) | VernacInclude (_) -> xlate_error "TODO : Include " - | VernacDeclareModuleType((_, id), bl, mty_o) -> + | VernacDeclareModuleType((_, id), bl, _, mty_o) -> CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with @@ -2045,18 +2044,18 @@ let rec xlate_vernac = CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT (xlate_module_type mty1) | _ -> failwith "TODO: Include Self") - | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) -> + | VernacDefineModule(_,(_, id), bl, mtys, mexpr_o) -> CT_module(xlate_ident id, xlate_module_binder_list bl, - xlate_module_type_check_opt mty_o, + xlate_module_type_check mtys, match mexpr_o with [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE | [m] -> xlate_module_expr m | _ -> failwith "TODO Include Self") - | VernacDeclareModule(_,(_, id), bl, mty_o) -> + | VernacDeclareModule(_,(_, id), bl, mty) -> CT_declare_module(xlate_ident id, xlate_module_binder_list bl, - xlate_module_type_check_opt (Some mty_o), + xlate_module_type_check (Topconstr.Enforce mty), CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE) | VernacRequire (impexp, spec, id::idl) -> let ct_impexp, ct_spec = get_require_flags impexp spec in |