diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
commit | a0a94c1340a63cdb824507b973393882666ba52a (patch) | |
tree | 73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /library/libnames.ml | |
parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) |
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 22 |
1 files changed, 17 insertions, 5 deletions
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 |