diff options
author | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-30 15:34:17 +0000 |
---|---|---|
committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-30 15:34:17 +0000 |
commit | 15910aaa912554401522c53b8bff5324d5b7dfaa (patch) | |
tree | d7a21c59a6339d06dcda9a09d684a88124f70524 /library/libnames.ml | |
parent | 65fe36d2ad32f2c46c67369555aa5f3461570b78 (diff) |
Correction bug 2037.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11873 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index b7b36afb3..f0fcd94c9 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 |