From 07b85674ef5f90467ea9bd8ed3c87572d2af8016 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 11 Jun 2008 14:35:13 +0000
Subject: Correction bug alias d'alias.

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

diff --git a/library/declaremods.ml b/library/declaremods.ml
index bb6d947c54..1b0cd86ae2 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1066,17 +1066,19 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 	mod_entry_expr = Some (MSEident mp) } ->
 	 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 prefix =  dir,(mp',empty_dirpath) in
 	 let mp1 = Environ.scrape_alias mp env in
+	 let prefix =  dir,(mp1,empty_dirpath) in
 	 let substituted = 
 	   match mbids with
 		    | [] -> 
 			Some (subst_objects prefix 
-				(join sub (join (map_msid msid mp') (map_mp mp' mp1))) objs)
+				(join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs)
 		    | _ -> None in
 	   ignore (add_leaf
 		     id
-		     (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted)));
+		     (in_module_alias (Some ({mod_entry_type = None;	    
+					      mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), 
+				       substobjs, substituted)));
 	   mmp
       | _ ->
 	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-- 
cgit v1.2.3