Report des commits 11417 et 11437 de la v8.2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7

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)
-