diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:43:16 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:43:16 +0000 |
commit | 2ab66d862fcfd8d730078ca79c74bbea37c206d6 (patch) | |
tree | a7f51ace899cfe961bb4a40ea663b4792296389c /library/nametab.mli | |
parent | f625fd3a414c3ae067e23320e382dbff5256adc4 (diff) |
Nouvelle structure arborescente à la Nametab pour prendre en compte les noms qualifiés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@866 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
-rwxr-xr-x | library/nametab.mli | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 463dc63de..2b0e4dd52 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -2,13 +2,31 @@ (* $Id$ *) (*i*) +open Util open Names +open Term (*i*) (* This module contains the table for globalization, which associates global names (section paths) to identifiers. *) -val push : identifier -> section_path -> unit +type cci_table = global_reference Idmap.t +type obj_table = (section_path * Libobject.obj) Idmap.t +type mod_table = module_contents Stringmap.t +and module_contents = Closed of cci_table * obj_table * mod_table + +val push : identifier -> global_reference -> unit +val push_obj : identifier -> (section_path * Libobject.obj) -> unit +val push_module : string -> module_contents -> unit + +val sp_of_id : path_kind -> identifier -> global_reference + +(* This returns the section_path of a constant or fails with Not_found *) +val constant_sp_of_id : identifier -> section_path + +val locate : section_path -> global_reference +val locate_obj : section_path -> (section_path * Libobject.obj) +val locate_constant : section_path -> constant_path + +val open_module_contents : string -> unit -val sp_of_id : path_kind -> identifier -> section_path -val fw_sp_of_id : identifier -> section_path |