From 15910aaa912554401522c53b8bff5324d5b7dfaa Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 30 Jan 2009 15:34:17 +0000
Subject: Correction bug 2037.

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

diff --git a/library/libnames.ml b/library/libnames.ml
index b7b36afb3c..f0fcd94c92 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -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