diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-24 12:57:10 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-24 12:57:10 +0000 |
| commit | 99c8c6f52ab04a7680340668a1677fe3e021d364 (patch) | |
| tree | d80e4c75f652afd02afbaa8bd4dc3870c43f6643 /library/nametab.mli | |
| parent | e870ab98ca09ee2f995fdaaa4e43cd95a9187a18 (diff) | |
Nametab data structure reorganisation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3030 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
| -rwxr-xr-x | library/nametab.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 7456f3a4c..11b6be271 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -76,9 +76,6 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a type visibility = Until of int | Exactly of int -(* is the short name visible? tests for 1 *) -val is_short_visible : visibility -> section_path -> bool - val push : visibility -> section_path -> global_reference -> unit val push_syntactic_definition : visibility -> section_path -> kernel_name -> unit @@ -123,7 +120,7 @@ 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 +val full_name_modtype : qualid -> section_path (*s Roots of the space of absolute names *) |