correction bug 1839

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

M    kernel/mod_typing.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@10829 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 57 insertions, 33 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 662841cdf..b1daea228 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -43,7 +43,7 @@ let rec check_with env mtb with_decl =
 	let cb = check_with_aux_def env mtb with_decl in
 	  SEBwith(mtb,With_definition_body(id,cb)),empty_subst
     | With_Module (id,mp) -> 
-	let cst,sub = check_with_aux_mod env mtb with_decl in
+	let cst,sub = check_with_aux_mod env mtb with_decl true in
 	  SEBwith(mtb,With_module_body(id,mp,cst)),sub
 
 and check_with_aux_def env mtb with_decl = 
@@ -116,7 +116,7 @@ and check_with_aux_def env mtb with_decl =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl = 
+and check_with_aux_mod env mtb with_decl now = 
   let initmsid,msid,sig_b = match (eval_struct env mtb) with 
     | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in
 	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
@@ -162,7 +162,12 @@ and check_with_aux_mod env mtb with_decl =
 		  | _,_ ->
 		      anomaly "Mod_typing:no implementation and no alias"
 	      in
-		cst,join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
+		if now then 
+		  let mp' = scrape_alias mp env' in
+		  let up_subst = update_subst_alias mtb'.typ_alias (map_mp (mp_rec [id]) mp') in
+		    cst, (join (map_mp (mp_rec [id]) mp') up_subst)
+		else
+		cst,empty_subst
         | With_Module (_::_,mp) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
@@ -175,11 +180,18 @@ and check_with_aux_mod env mtb with_decl =
 			  With_Definition (_,c) -> 
 			    With_Definition (idl,c)
 			| With_Module (_,c) -> With_Module (idl,c) in
-		      let cst,sub =
+		      let cst,_ =
 			check_with_aux_mod env' 
-			  (type_of_mb env old) new_with_decl in
-			cst,(join (map_mp (mp_rec idl) mp) sub)
-                  | Some msb ->
+			  (type_of_mb env old) new_with_decl false in
+			if now then 
+			  let mtb' = lookup_modtype mp env' in
+			  let mp' = scrape_alias mp env' in
+			  let up_subst = update_subst_alias 
+			    mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in
+			    cst, (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst)
+		else
+		cst,empty_subst
+		  | Some msb ->
                       error_a_generative_module_expected l
               end
 	| _ -> anomaly "Modtyping:incorrect use of with"
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4d0af4fee..0d0af00f0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -270,17 +270,19 @@ let rec eval_struct env = function
 			   (join sub_alias 
 			      (map_mbid farg_id mp (Some resolve))) fbody_b)
   | SEBwith (mtb,(With_definition_body _ as wdb)) ->
-      merge_with env mtb wdb empty_subst
+      let mtb',_ = merge_with env mtb wdb empty_subst in
+	mtb'
   | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
       let alias_in_mp =
 	(lookup_modtype mp env).typ_alias in
       let alias_in_mp = match eval_struct env (SEBident mp) with
 	| SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp
 	| _ -> alias_in_mp in
-	merge_with env mtb wdb alias_in_mp
+      let mtb',_ = merge_with env mtb wdb alias_in_mp in
+	mtb'
 (*  | SEBfunctor(mbid,mtb,body) -> 
-      let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
-	SEBfunctor(mbid,mtb,eval_struct env body) *)
+    let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
+    SEBfunctor(mbid,mtb,eval_struct env body) *)
   | mtb -> mtb
       
 and type_of_mb env mb =
@@ -328,25 +330,28 @@ and merge_with env mtb with_decl alias=
                   With_definition_body (_,c) -> With_definition_body (idl,c),None
 		| With_module_body (idc,mp,cst) -> 
 		    With_module_body (idl,mp,cst),
-		      Some(map_mp (mp_rec idc) mp) 
+		      Some(map_mp (mp_rec (List.rev idc)) mp) 
 	    in
-	    let subst1 = match subst1 with
+	    let subst = match subst1 with
 	      | None -> None
-	      | Some s -> Some (update_subst_alias alias s) in
-	    let subst = Option.fold_right join subst1 alias in
-            let modtype = 
+	      | Some s -> Some (join s (update_subst_alias alias s)) in
+            let modtype,subst_msb = 
               merge_with env (type_of_mb env old) new_with_decl alias in
             let msb =
 	      { mod_expr = None;
 		mod_type = Some modtype; 
 		mod_constraints = old.mod_constraints;
-		mod_alias = subst;
+		mod_alias = begin 
+		  match subst_msb with
+		    |None -> empty_subst
+		    |Some s -> s
+		end;
 		mod_retroknowledge = old.mod_retroknowledge}
 	    in
-	      (SFBmodule msb),Some subst
+	      (SFBmodule msb),subst
       in
 	SEBstruct(msid,  before@(l,new_spec)::
-		    (Option.fold_right subst_structure subst after))
+		    (Option.fold_right subst_structure subst after)),subst
     with
 	Not_found -> error_no_such_label l
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index e4b1f7045..a24f835d9 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -300,6 +300,7 @@ let rec check_modules cst env msid1 l msb1 msb2 =
 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 sig2 = subst_signature_msid msid2 mp1 sig2 in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3907ab21b..93e322e2c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -538,7 +538,7 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
 	    else error "MODULE expected!"
 	| idl,lobj::tail -> lobj::replace_idl (idl,tail)
       in
-	(join (map_mp (mp_rec idl) mp) subst, mbids, msid, replace_idl (idl,lib_stack))
+	(join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack))
 	  
 let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
   (subst, mbids1@mbids2, msid, lib_stack)
@@ -554,7 +554,7 @@ let rec get_modtype_substobjs env = function
       let modobjs = MPmap.find mp !modtab_substobjs in
 	replace_module_object idl substobjs modobjs mp
   | MSEapply (mexpr, MSEident mp) ->
-      let ftb,_ = Mod_typing.translate_struct_entry env mexpr in
+     let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
       let farg_id, farg_b, fbody_b = Modops.destr_functor env 
 	(Modops.eval_struct env ftb) in
       let mp = Environ.scrape_alias mp env in
@@ -564,18 +564,22 @@ let rec get_modtype_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-      let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in
-      let sub_alias = update_subst_alias sub_alias 
-	(map_mbid farg_id mp (None)) in
-      let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+      let sub3 = update_subst_alias sub_alias
+	(join_alias sub1 (map_mbid farg_id mp None)) 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_modtype_substobjs env mexpr in
 	(match mbids with
 	   | mbid::mbids ->
                let resolve =
 		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
-		 (join (join subst (map_mbid mbid mp (Some resolve))) sub_alias
-		    , mbids, msid, objs)
+		((join 
+		    (join subst (map_mbid mbid mp (Some resolve)))
+		       sub)
+		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
 	       | _ -> error "Application of a functor with too few arguments")
@@ -862,7 +866,7 @@ let rec get_module_substobjs env = function
        let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
 	(subst, mbid::mbids, msid, objs)
   | MSEapply (mexpr, MSEident mp) ->
-      let ftb,_ = Mod_typing.translate_struct_entry env mexpr in
+      let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
       let farg_id, farg_b, fbody_b = Modops.destr_functor env 
 	(Modops.eval_struct env ftb) in
       let mp = Environ.scrape_alias mp env in
@@ -872,10 +876,12 @@ let rec get_module_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-      let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in
-      let sub_alias = update_subst_alias sub_alias 
-	(map_mbid farg_id mp (None)) in
-      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+      let sub3 = update_subst_alias sub_alias
+	(join_alias sub1 (map_mbid farg_id mp None)) 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 ->
                let resolve =
@@ -884,7 +890,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_alias)
+		       sub)
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"