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/safe_typing.ml | |
| parent | c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (diff) | |
Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 9 |
1 files changed, 2 insertions, 7 deletions
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 *) |