From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- library/nametab.mli | 49 +++++++++++++++++++++++++++---------------------- 1 file changed, 27 insertions(+), 22 deletions(-) (limited to 'library/nametab.mli') 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 *) -(* 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 -- cgit v1.2.3