diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 14:58:39 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 14:58:39 +0100 |
commit | 83e82ef7b42f47d63d3b40b2698695a0e7b2d685 (patch) | |
tree | ef1ab4f39e6aec01d6ab5a37beed8709204711ac /kernel | |
parent | c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (diff) |
Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/mod_typing.ml | 12 | ||||
-rw-r--r-- | kernel/mod_typing.mli | 14 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 9 |
3 files changed, 19 insertions, 16 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index eef83ce74..c03c5175f 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -351,12 +351,20 @@ let translate_module env mp inl = function let restype = Option.map (fun ty -> ((params,ty),inl)) oty in finalize_module env mp t restype -let rec translate_mse_incl env mp inl = function +let rec translate_mse_inclmod env mp inl = function |MEident mp1 -> let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in let sign = clean_bounded_mod_expr mb.mod_type in sign,None,mb.mod_delta,Univ.ContextSet.empty |MEapply (fe,arg) -> - let ftrans = translate_mse_incl env mp inl fe in + let ftrans = translate_mse_inclmod env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) |MEwith _ -> assert false (* No 'with' syntax for modules *) + +let translate_mse_incl is_mod env mp inl me = + if is_mod then + translate_mse_inclmod env mp inl me + else + let mtb = translate_modtype env mp inl ([],me) in + let sign = clean_bounded_mod_expr mtb.mod_type in + sign,None,mtb.mod_delta,mtb.mod_constraints diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 0c3fb2ba7..bc0e20205 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,14 +36,14 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation -(** [translate_mse_incl] translate the mse of a real module (no - module type here) given to an Include *) - -val translate_mse_incl : - env -> module_path -> inline -> module_struct_entry -> - module_alg_expr translation - val finalize_module : env -> module_path -> module_expression translation -> (module_type_entry * inline) option -> module_body + +(** [translate_mse_incl] translate the mse of a module or + module type given to an Include *) + +val translate_mse_incl : + bool -> env -> module_path -> inline -> module_struct_entry -> + module_alg_expr translation diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fdacbb365..ec245b064 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -682,13 +682,8 @@ let end_modtype l senv = let add_include me is_module inl senv = let open Mod_typing in let mp_sup = senv.modpath in - let sign,cst,resolver = - if is_module then - let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in - sign,cst,reso - else - let mtb = translate_modtype senv.env mp_sup inl ([],me) in - mtb.mod_type,mtb.mod_constraints,mtb.mod_delta + let sign,_,resolver,cst = + translate_mse_incl is_module senv.env mp_sup inl me in let senv = add_constraints (Now (false, cst)) senv in (* Include Self support *) |