diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index eef2d675ce..09b2f918f0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -27,6 +27,7 @@ open Subtyping open Mod_typing open Mod_subst + type modvariant = | NONE | SIG of (* funsig params *) (mod_bound_id * module_type_body) list @@ -312,6 +313,13 @@ let add_alias l mp senv = check_label l senv.labset; let mp' = MPdot(senv.modinfo.modpath, l) in let mp1 = scrape_alias mp senv.env in + let typ_opt = + if check_bound_mp mp then + Some (strengthen senv.env + (lookup_modtype mp senv.env).typ_expr mp) + else + None + in (* we get all updated alias substitution {mp1.K\M} that comes from mp1 *) let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in (* transformation of {mp1.K\M} to {mp.K\M}*) @@ -327,7 +335,7 @@ let add_alias l mp senv = alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp,None))::senv.revstruct; + revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -502,7 +510,7 @@ let end_module l restype senv = imports = senv'.imports; loads = senv'.loads; local_retroknowledge = senv'.local_retroknowledge } - | SFBalias (mp',cst) -> + | SFBalias (mp',typ_opt,cst) -> let env' = Option.fold_right Environ.add_constraints cst senv.env in let mp = MPdot(senv.modinfo.modpath, l) in @@ -518,7 +526,7 @@ let end_module l restype senv = alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp',cst))::senv.revstruct; + revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -817,4 +825,3 @@ let j_type j = j.uj_type let safe_infer senv = infer (env_of_senv senv) let typing senv = Typeops.typing (env_of_senv senv) - |