diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
| commit | a6d858b84132bcb27bcc771f06a854cc94eef716 (patch) | |
| tree | df016a77a6d8d2f2a43fa9c2c01adc09b3be7c1b /library/global.ml | |
| parent | 000ece141dc22e35365ea81558e8b6b1e65bd54c (diff) | |
Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 1f509bcde..b55f741dd 100644 --- a/library/global.ml +++ b/library/global.ml @@ -78,9 +78,9 @@ let qualid_of_global ref = if (try Nametab.locate qid = ref with Not_found -> false) then qid else match dir with | [] -> Nametab.qualid_of_sp sp - | a::l -> find_visible l (a::qdir) + | a::l -> find_visible l (add_dirpath_prefix a qdir) in - find_visible (List.rev (dirpath sp)) [] + find_visible (rev_repr_dirpath (dirpath sp)) (make_dirpath []) let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref) |