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

3 files changed, 37 insertions, 19 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 662841cdfb..b1daea2287 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 4d0af4fee5..0d0af00f09 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 e4b1f7045c..a24f835d96 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