diff options
Diffstat (limited to 'library/nametab.mli')
-rw-r--r-- | library/nametab.mli | 49 |
1 files changed, 27 insertions, 22 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 79ea119b..e3aeb675 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,15 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Names open Libnames +open Globnames (** This module contains the tables for globalization. *) @@ -17,7 +17,7 @@ open Libnames qualified names (qualid). There are three classes of names: - 1a) internal kernel names: [kernel_name], [constant], [inductive], - [module_path], [dir_path] + [module_path], [DirPath.t] - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... @@ -33,7 +33,7 @@ open Libnames Registers the [object_reference] to be referred to by the [full_user_name] (and its suffixes according to [visibility]). - [full_user_name] can either be a [full_path] or a [dir_path]. + [full_user_name] can either be a [full_path] or a [DirPath.t]. } {- [exists : full_user_name -> bool] @@ -51,19 +51,17 @@ open Libnames {- [shortest_qualid_of : object_reference -> user_name] The [user_name] can be for example the shortest non ambiguous [qualid] or - the [full_user_name] or [identifier]. Such a function can also have a + the [full_user_name] or [Id.t]. Such a function can also have a local context argument.}} *) exception GlobalizationError of qualid -exception GlobalizationConstantError of qualid (** Raises a globalization error *) -val error_global_not_found_loc : loc -> qualid -> 'a +val error_global_not_found_loc : Loc.t -> qualid -> 'a val error_global_not_found : qualid -> 'a -val error_global_constant_not_found_loc : loc -> qualid -> 'a (** {6 Register visibility of things } *) @@ -79,7 +77,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit val push_modtype : visibility -> full_path -> module_path -> unit -val push_dir : visibility -> dir_path -> global_dir_reference -> unit +val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit type ltac_constant = kernel_name @@ -98,7 +96,7 @@ val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path -val locate_section : qualid -> dir_path +val locate_section : qualid -> DirPath.t val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global @@ -113,6 +111,9 @@ val global_inductive : reference -> inductive val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list +val locate_extended_all_tactic : qualid -> ltac_constant list +val locate_extended_all_dir : qualid -> global_dir_reference list +val locate_extended_all_modtype : qualid -> module_path list (** Mapping a full path to a global reference *) @@ -123,15 +124,16 @@ val extended_global_of_path : full_path -> extended_global_reference val exists_cci : full_path -> bool val exists_modtype : full_path -> bool -val exists_dir : dir_path -> bool -val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *) -val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *) +val exists_dir : DirPath.t -> bool +val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *) (** {6 These functions locate qualids into full user names } *) val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path -val full_name_module : qualid -> dir_path +val full_name_module : qualid -> DirPath.t (** {6 Reverse lookup } Finding user names corresponding to the given @@ -142,25 +144,28 @@ val full_name_module : qualid -> dir_path val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> dir_path +val dirpath_of_module : module_path -> DirPath.t +val path_of_modtype : module_path -> full_path val path_of_tactic : ltac_constant -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> dir_path -val basename_of_global : global_reference -> identifier +val dirpath_of_global : global_reference -> DirPath.t +val basename_of_global : global_reference -> Id.t -(** Printing of global references using names as short as possible *) -val pr_global_env : Idset.t -> global_reference -> std_ppcmds +(** Printing of global references using names as short as possible. + @raise Not_found when the reference is not in the global tables. *) +val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds (** The [shortest_qualid] functions given an object with [user_name] Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and - Coq.A.B.x that denotes the same object. *) + Coq.A.B.x that denotes the same object. + @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid +val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid +val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : module_path -> qualid val shortest_qualid_of_module : module_path -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid |