correction bug 1839

is line, and those below, will be ignored--

M    kernel/mod_subst.mli
M    kernel/mod_typing.ml
M    kernel/mod_subst.ml
M    kernel/subtyping.ml
M    kernel/modops.ml
M    library/declaremods.ml


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

6 files changed, 85 insertions, 31 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 0df3e6631..040d7f811 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -347,6 +347,48 @@ let update_subst_alias subst1 subst2 =
   in
     Umap.fold alias_subst subst1 empty_subst
 
+let update_subst subst1 subst2 =
+ let subst_inv key (mp,resolve) l =
+    let newmp = 
+      match key with 
+	| MBI msid -> MPbound msid
+	| MSI msid -> MPself msid
+	| MPI mp -> mp
+    in
+   match mp with 
+     | MPbound mbid ->  ((MBI mbid),newmp)::l
+     | MPself msid ->  ((MSI msid),newmp)::l
+     | _ ->   ((MPI mp),newmp)::l
+  in 
+  let subst_mbi = Umap.fold subst_inv subst2 [] in
+  let alias_subst key (mp,resolve) sub=
+    let newsetkey = 
+      match key with
+	| MPI mp1 -> 
+	    let compute_set_newkey l (k,mp') = 
+	      let mp_from_key = match k with
+		  	| MBI msid -> MPbound msid
+			| MSI msid -> MPself msid
+			| MPI mp -> mp
+	      in
+	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
+		if new_mp1 == mp1 then l else (MPI new_mp1)::l
+	    in
+	    begin
+	      match List.fold_left compute_set_newkey [] subst_mbi with
+		| [] -> None
+		| l -> Some (l)
+	    end
+	| _ -> None
+    in
+      match newsetkey with
+	| None -> sub
+	| Some l -> 
+	    List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+	      sub l
+  in
+    Umap.fold alias_subst subst1 empty_subst
+
 let join_alias (subst1 : substitution) (subst2 : substitution) =
   let apply_subst (sub : substitution) key (mp,resolve) =
     let mp',resolve' =
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 5384d0f85..6ae9649d6 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -85,6 +85,8 @@ val occur_mbid : mod_bound_id -> substitution -> bool
 
 val update_subst_alias : substitution -> substitution -> substitution
 
+val update_subst : substitution -> substitution -> substitution
+
 val subst_key : substitution -> substitution -> substitution
 
 val join_alias : substitution -> substitution -> substitution
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 09edc63f6..4a2dd9afc 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -263,27 +263,25 @@ and translate_struct_entry env mse = match mse with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
       let meb,sub2= translate_struct_entry env (MSEident mp) in
-      let sub2 = match eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub2
-	| _ -> sub2 in
-       let sub3=
-	if sub1 = empty_subst then
-	  update_subst_alias sub2 (map_mbid farg_id mp None)
+	if sub1 = empty_subst then 
+	  let cst = check_subtypes env mtb farg_b in
+	    SEBapply(feb,meb,cst),sub1
 	else
-	  update_subst_alias sub2
-	    (join_alias sub1 (map_mbid farg_id mp None))
-       in
-      let sub = if sub2 = sub3 then
-	join sub1 sub2 else join (join sub1 sub2) sub3 in
-      let sub = join_alias sub (map_mbid farg_id mp None) in
-      let sub = update_subst_alias sub (map_mbid farg_id mp None) in
-      let cst = check_subtypes env mtb farg_b in
-	SEBapply(feb,meb,cst),sub
+	  let sub2 = match eval_struct env (SEBident mp) with
+	    | SEBstruct (msid,sign) -> 
+		join_alias 
+		  (subst_key (map_msid msid mp) sub2)
+		  (map_msid msid mp)
+	    | _ -> sub2 in
+	  let sub3 = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub4 = update_subst sub2 sub3 in
+	  let cst = check_subtypes env mtb farg_b in
+	    SEBapply(feb,meb,cst),(join sub3 sub4)
   | MSEwith(mte, with_decl) ->
 	let mtb,sub1 = translate_struct_entry env mte in
 	let mtb',sub2 = check_with env mtb with_decl in
 	  mtb',join sub1 sub2
-
+	    
 
 let rec add_struct_expr_constraints env = function
   | SEBident _ -> env
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 590db2727..49e49f573 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,8 +329,9 @@ and merge_with env mtb with_decl alias=
 	      match with_decl with
                   With_definition_body (_,c) -> With_definition_body (idl,c),None
 		| With_module_body (idc,mp,cst) -> 
+		    let mp' = scrape_alias mp env in
 		    With_module_body (idl,mp,cst),
-		      Some(map_mp (mp_rec (List.rev idc)) mp) 
+		      Some(map_mp (mp_rec (List.rev idc)) mp') 
 	    in
 	    let subst = match subst1 with
 	      | None -> None
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index a24f835d9..0c31d7962 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -289,9 +289,16 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        check_conv cst conv env ty1 ty2
    | _ -> error ()
 	      
-let rec check_modules cst env msid1 l msb1 msb2 =
+let rec check_modules cst env msid1 l msb1 msb2 alias =
   let mp = (MPdot(MPself msid1,l)) in
   let mty1 = module_type_of_module (Some mp) msb1 in
+  let alias1,struct_expr = match eval_struct env mty1.typ_expr with
+    	| SEBstruct (msid,sign) as str ->
+	    update_subst alias (map_msid msid mp),str
+	| _ as str -> empty_subst,str in
+  let mty1 = {mty1 with 
+		typ_expr = struct_expr;
+		typ_alias = join alias1 mty1.typ_alias } in
   let mty2 =  module_type_of_module None msb2 in
   let cst = check_modtypes cst env mty1 mty2 false in
     cst
@@ -301,8 +308,8 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
   let mp1 = MPself msid1 in
   let env = add_signature mp1 sig1 env in 
   let sig1 = subst_structure alias sig1 in
-  let alias = update_subst_alias alias (map_msid msid2 mp1) in
-  let sig2 = subst_structure alias sig2' in
+  let alias1 = update_subst_alias alias (map_msid msid2 mp1) in
+  let sig2 = subst_structure alias1 sig2' in
   let sig2 = subst_signature_msid msid2 mp1 sig2 in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
@@ -321,14 +328,14 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
 	| SFBmodule msb2 ->  
 	    begin
 	      match info1 with
-		| Module msb -> check_modules cst env msid1 l msb msb2
+		| Module msb -> check_modules cst env msid1 l msb msb2 alias
 		| Alias mp ->let msb = 
 		    {mod_expr = Some (SEBident mp);
 		     mod_type = Some (eval_struct env (SEBident mp));
 		     mod_constraints = Constraint.empty;
 		     mod_alias = (lookup_modtype mp env).typ_alias;
 		     mod_retroknowledge = []} in
-		    check_modules cst env msid1 l msb msb2
+		    check_modules cst env msid1 l msb msb2 alias
 		| _ -> error_not_match l spec2
 	    end
 	| SFBalias (mp,_) ->
@@ -342,7 +349,7 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
 		       mod_constraints = Constraint.empty;
 		       mod_alias = (lookup_modtype mp env).typ_alias;
 		       mod_retroknowledge = []} in
-			check_modules cst env msid1 l msb msb1
+			check_modules cst env msid1 l msb msb1 alias
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5f7daa9b5..59da90e66 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -332,7 +332,9 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
   check_empty "subst_module" entry;
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
   let (sub,mbids,msid,objs) = substobjs in
+  let sub = subst_key subst sub in
   let sub' = update_subst_alias subst sub in
+  let sub' = update_subst_alias sub' (map_msid msid mp) in
   let sub = join sub' sub in
   let subst' = join sub subst in
   (* substitutive_objects get the new substitution *)
@@ -346,6 +348,7 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
 let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
   let (sub,mbids,msid,objs) = substobjs in
+  let sub = update_subst_alias subst (map_msid msid mp) in
   let subst' = join sub subst in
   (* substitutive_objects get the new substitution *)
   let substobjs = (subst',mbids,msid,objs) in
@@ -365,8 +368,8 @@ let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
 		  substobjs, match mbids with
 		    | [] -> 
 			Some (subst_objects prefix 
-				(join (map_mp mp mp')
-				   (join (map_msid msid mp') subst)) objs)
+				(join subst' (join (map_msid msid mp')
+						(map_mp mp mp'))) objs)
 		    | _ -> None)
 
 	      | _ -> anomaly "Modops: Not an alias"
@@ -886,12 +889,10 @@ let rec get_module_substobjs env = function
 	if sub1 = empty_subst then
 	  update_subst_alias sub_alias (map_mbid farg_id mp None)
 	else
-	  update_subst_alias sub_alias
-	    (join_alias sub1 (map_mbid farg_id mp None))
+	  let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub_alias' =  update_subst_alias sub_alias sub1' in
+	    join sub1' sub_alias'
       in
-      let sub = if sub_alias = sub3 then
-	join sub1 sub_alias else join (join sub1 sub_alias) sub3 in
-      let sub = join_alias sub (map_mbid farg_id mp None) in
        let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
 	(match mbids with
 	   | mbid::mbids ->
@@ -901,7 +902,7 @@ let rec get_module_substobjs env = function
                     objects (that are all non-logical objects) *)
 		((join 
 		    (join subst (map_mbid mbid mp (Some resolve)))
-		       sub)
+		       sub3)
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
@@ -1072,6 +1073,9 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 		     (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted)))
       | _ ->
 	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+	  let (sub,mbids,msid,objs) = substobjs in
+	  let sub' = subst_key (map_msid msid mp) sub in
+	  let substobjs = (join sub sub',mbids,msid,objs) in
 	  let substituted = subst_substobjs dir mp substobjs in
 	    ignore (add_leaf
 		      id