From d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 15 Oct 2008 15:07:10 +0000
Subject: Report des commits 11417 et 11437 de la v8.2

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

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index ac5636b58e..72f199efb5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -434,10 +434,12 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
 			 mod_entry_expr = 
 			      Some (MSEident mp')},sub),
 		    substobjs, match mbids with
-		      | [] -> 
+		      | [] -> let subst = update_subst subst' (map_mp mp' mp) in
 			  Some (subst_objects (dir,(mp',empty_dirpath)) 
-				  (join subst' (join (map_msid msid mp')
-						  (map_mp mp mp'))) objs)
+				  (join (join subst' subst) (join (map_msid msid mp')
+						  (map_mp mp mp')))
+				   objs)
+
 		      | _ -> None)
 		     
 	      | _ -> anomaly "Modops: Not an alias"
-- 
cgit v1.2.3