From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 19 Feb 2009 13:13:14 +0100
Subject: Imported Upstream version 8.2-1+dfsg

---
 library/libnames.ml | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'library/libnames.ml')

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
-- 
cgit v1.2.3