From ec3f3aed78e6c31ce819723a35efd68474d8c006 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Thu, 3 Apr 2008 16:44:48 +0000
Subject: Correction bug 1818, 3eme commentaire. mauvaise generation de
 substitution a l'application du foncteur.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10747 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declaremods.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7c228741b4..bc1fa6f24a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -287,6 +287,8 @@ let subst_substobjs dir mp (subst,mbids,msid,objs) =
   match mbids with
     | [] -> 
 	let prefix = dir,(mp,empty_dirpath) in
+	let subst' = join_alias (map_msid msid mp) subst in
+	let subst = join subst' subst in
 	  Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
     | _ -> None
 
@@ -355,14 +357,16 @@ let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
 	  begin
 	    match me with
 	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp)} ->
-		 let mp = subst_mp subst' mp in
+		mod_entry_expr = Some (MSEident mp')} ->
+		 let mp' = subst_mp subst' mp' in
 		 (Some ({mod_entry_type = None;
 			 mod_entry_expr = 
-			    Some (MSEident mp)},sub),
+			    Some (MSEident mp')},sub),
 		  substobjs, match mbids with
 		    | [] -> 
-			Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
+			Some (subst_objects prefix 
+				(join (map_mp mp mp')
+				   (join (map_msid msid mp') subst)) objs)
 		    | _ -> None)
 
 	      | _ -> anomaly "Modops: Not an alias"
-- 
cgit v1.2.3