Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg

3 files changed, 22 insertions, 7 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index de1893c7..3026143b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11703 2008-12-18 15:54:41Z soubiran $ i*)
+(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -628,6 +628,7 @@ let rec get_modtype_substobjs env = function
   | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
   | MSEwith (mty, With_Module (idl,mp)) -> 
       let substobjs = get_modtype_substobjs env mty in
+      let mp = Environ.scrape_alias mp env in
       let modobjs = MPmap.find mp !modtab_substobjs in
 	replace_module_object idl substobjs modobjs mp
   | MSEapply (mexpr, MSEident mp) ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 3f226179..89a77128 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 11750 2009-01-05 20:47:34Z herbelin $ i*)
+(*i $Id: libnames.ml 11878 2009-02-03 12:48:18Z soubiran $ i*)
 
 open Pp
 open Util
@@ -199,11 +199,23 @@ let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
 
 let decode_kn kn = 
+  let rec dir_of_mp = function
+    | MPfile dir -> repr_dirpath dir
+    | MPbound mbid -> 
+	let _,_,dp = repr_mbid mbid in
+	let id = id_of_mbid mbid in
+	  id::(repr_dirpath dp)
+    | MPself msid -> 
+	let _,_,dp = repr_msid msid in
+	let id = id_of_msid msid in
+	  id::(repr_dirpath dp) 
+    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+  in
   let mp,sec_dir,l = repr_kn kn in
-    match mp,(repr_dirpath sec_dir) with
-	MPfile dir,[] -> (dir,id_of_label l)
-      | _ , [] -> anomaly "MPfile expected!"
-      | _ -> anomaly "Section part should be empty!"
+    if (repr_dirpath sec_dir) = [] then
+     (make_dirpath (dir_of_mp mp)),id_of_label l
+    else
+      anomaly "Section part should be empty!"
 
 let decode_con kn = 
   let mp,sec_dir,l = repr_con kn in
diff --git a/library/library.ml b/library/library.ml
index 9f3478f0..0e1342f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -629,6 +629,8 @@ let error_recursively_dependent_library dir =
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
+(* Security weakness: file might have been changed on disk between
+   writing the content and computing the checksum... *) 
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
   let md = {