diff options
| author | herbelin | 2001-03-01 14:02:59 +0000 |
|---|---|---|
| committer | herbelin | 2001-03-01 14:02:59 +0000 |
| commit | 7b6ed1e95bef26f4ae85d7471985128c0dfdbc15 (patch) | |
| tree | a2beab552c8e57d5db2833494e5cc79e6374cc84 /library/global.mli | |
| parent | 2a9a43be51ac61e04ebf3fce902899155b48057f (diff) | |
Déplacement de qualid dans Nametab, hors du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index 74a7197d4b..da0386be1d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -49,7 +49,10 @@ val import : compiled_env -> unit (*s Some functions of [Environ] instanciated on the global environment. *) val sp_of_global : global_reference -> section_path -val qualid_of_global : global_reference -> qualid + +(*s This is for printing purpose *) +val qualid_of_global : global_reference -> Nametab.qualid +val string_of_global : global_reference -> string (*s Function to get an environment from the constants part of the global environment and a given context. *) |