diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 14:44:24 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 14:44:24 +0000 |
commit | a3848b0a10064fb7e206a503ac8b829cb9ce4666 (patch) | |
tree | 57715eb46564f71b91825c46ecb432a41c1ec095 /library/nametab.mli | |
parent | bc4e7b8c2317b2536eb42efb7cbf37d748ceb7c6 (diff) |
Petites corrections ici et la
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
-rwxr-xr-x | library/nametab.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index b64fe0d9d..626a529e6 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -120,6 +120,8 @@ val exists_dir : dir_path -> bool val exists_section : dir_path -> bool (* deprecated *) val exists_module : dir_path -> bool (* deprecated *) +val full_name_modtype : qualid -> kernel_name * section_path + (*s Roots of the space of absolute names *) (* This turns a "user" absolute name into a global reference; |