diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/global.ml | 13 | ||||
-rw-r--r-- | library/global.mli | 3 |
2 files changed, 14 insertions, 2 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. *) diff --git a/library/global.mli b/library/global.mli index 0dcaef62a..05af78a01 100644 --- a/library/global.mli +++ b/library/global.mli @@ -47,7 +47,8 @@ val import : compiled_env -> unit (*s Some functions of [Environ] instanciated on the global environment. *) -val id_of_global : global_reference -> identifier +val sp_of_global : global_reference -> section_path +val qualid_of_global : global_reference -> qualid (*s Function to get an environment from the constants part of the global environment and a given context. *) |