Correction de bugs relatifs a la compostion des substitutions

engendrees par les alias de module



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

4 files changed, 28 insertions, 16 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ea477d6a1..3b3d28090 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -320,16 +320,14 @@ let update_subst_alias subst1 subst2 =
  let subst_inv key (mp,resolve) sub =
     let newmp = 
       match key with 
-	| MBI msid -> Some (MPbound msid)
-	| MSI msid -> Some (MPself msid)
-	| _ -> None
+	| MBI msid -> MPbound msid
+	| MSI msid -> MPself msid
+	| MPI mp -> mp
     in
-      match newmp with
-	| None -> sub
-	| Some mpi -> match mp with 
-	    | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
-	    | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
-	    | _ ->  Umap.add (MPI mp) (mpi,None) sub
+   match mp with 
+     | MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub
+     | MPself msid -> Umap.add (MSI msid) (newmp,None) sub
+     | _ ->  Umap.add (MPI mp) (newmp,None) sub
   in 
   let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
   let alias_subst key (mp,resolve) sub=
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3ae9293c7..36ef0c5e6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -243,16 +243,22 @@ and translate_struct_entry env mse = match mse with
       let feb'= eval_struct env feb
       in
       let farg_id, farg_b, fbody_b = destr_functor env feb' in
-      let mtb = 
+      let mtb,mp = 
 	try
-	  lookup_modtype (path_of_mexpr mexpr) env
+	  let mp = path_of_mexpr mexpr in
+	  lookup_modtype mp env,mp
 	with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
       let meb,sub2= translate_struct_entry env mexpr in
-      let sub = join sub1 sub2 in
-      let sub = join_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
-      let sub = update_subst_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
+      let sub2 = match eval_struct env (SEBident mp) with
+	| SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub2
+	| _ -> sub2 in
+      let sub3 = 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
   | MSEwith(mte, with_decl) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index dc339af52..8d74c4c30 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -271,6 +271,9 @@ let rec eval_struct env = function
   | 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
 (*  | SEBfunctor(mbid,mtb,body) -> 
       let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
@@ -308,8 +311,9 @@ and merge_with env mtb with_decl alias=
 	    SFBconst c,None
 	| With_module_body ([id], mp,cst) ->
 	    let mp' = scrape_alias mp env in
+	    let new_alias = update_subst_alias alias (map_mp (mp_rec [id]) mp') in
 	      SFBalias (mp,Some cst),
-	    Some(join (map_mp (mp_rec [id]) mp') alias)
+	    Some(join (map_mp (mp_rec [id]) mp') new_alias)
 	| With_definition_body (_::_,_) 
         | With_module_body (_::_,_,_) -> 
 	    let old = match spec with
@@ -323,6 +327,9 @@ and merge_with env mtb with_decl alias=
 		    With_module_body (idl,mp,cst),
 		      Some(map_mp (mp_rec idc) mp) 
 	    in
+	    let subst1 = 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 = 
               merge_with env (type_of_mb env old) new_with_decl alias in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b1eea3bbd..a895e68ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -311,7 +311,8 @@ let add_alias l mp senv =
   (* we get all alias substitutions that comes from mp *)
   let _,sub = translate_struct_entry senv.env (MSEident mp) in
    (* we add the new one *)
-  let sub = join (map_mp mp' mp) sub in
+  let mp1 = scrape_alias mp senv.env in
+  let sub = join (map_mp mp' mp1) sub in
   let env' = register_alias mp' mp senv.env in
     mp', { old = senv.old;
 	env = env';