diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 18:52:04 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 18:52:04 +0000 |
commit | 85b4184369459fff82a11bd2708c10d77f10e9fd (patch) | |
tree | 45f8bca69d83804504c087955291e2cd69e5843f /library/nametab.mli | |
parent | a0b087a6e16a22b12c8520b81a1526bdda888cd3 (diff) |
Prise en compte de noms absolus dans la nametab
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
-rwxr-xr-x | library/nametab.mli | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 54c4bc67b..1d39eb310 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -12,12 +12,12 @@ open Term type cci_table = global_reference Stringmap.t type obj_table = (section_path * Libobject.obj) Stringmap.t -type mod_table = module_contents Stringmap.t +type mod_table = (section_path * module_contents) Stringmap.t and module_contents = Closed of cci_table * obj_table * mod_table -val push : identifier -> global_reference -> unit -val push_object : identifier -> (section_path * Libobject.obj) -> unit -val push_module : string -> module_contents -> unit +val push : section_path -> global_reference -> unit +val push_object : section_path -> Libobject.obj -> unit +val push_module : section_path -> module_contents -> unit val sp_of_id : path_kind -> identifier -> global_reference @@ -27,9 +27,13 @@ val constant_sp_of_id : identifier -> section_path val locate : qualid -> global_reference val locate_obj : qualid -> (section_path * Libobject.obj) val locate_constant : qualid -> constant_path +val locate_module : qualid -> section_path * module_contents -val open_module_contents : string -> unit -val rec_open_module_contents : string -> unit +(* [exists sp] tells if [sp] is already bound to a cci term *) +val exists_cci : section_path -> bool + +val open_module_contents : qualid -> unit +val rec_open_module_contents : qualid -> unit |