diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /kernel/safe_typing.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
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 3c7461b2..fbb05a2d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *) open Util open Names @@ -312,6 +312,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 +334,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 +509,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 +525,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; |