Fonction qualid_of_global pour affichage des paths avec des '.'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@927 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 1 deletions

diff --git a/library/global.ml b/library/global.ml
index 6a2dfe145..d5885ed02 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Util
+open Names
 open Term
 open Instantiate
 open Sign
@@ -55,7 +56,17 @@ let import cenv = global_env := import cenv !global_env
 
 (* Some instanciations of functions from [Environ]. *)
 
-let id_of_global id = Environ.id_of_global (env_of_safe_env !global_env) id
+let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id
+
+(* To know how qualified a name should be to be understood in the current env*)
+
+let is_visible ref qid = (Nametab.locate qid = ref)
+
+let qualid_of_global ref =  
+  let sp = sp_of_global ref in
+  let qid = make_qualid [] (string_of_id (basename sp)) in
+  if is_visible ref qid then qid
+  else make_qualid (dirpath sp) (string_of_id (basename sp))
 
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)