From 1a6a26d29252da54b86bf663a66ddd909905d1cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 Oct 2017 14:06:29 +0200 Subject: Moving the Ltac-specific part of the nametab to the Ltac plugin. For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit. --- library/nametab.mli | 9 --------- 1 file changed, 9 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 025a63b1c..3a380637c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -78,10 +78,6 @@ val push_modtype : visibility -> full_path -> module_path -> 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 -val push_tactic : visibility -> full_path -> ltac_constant -> unit - - (** {6 The following functions perform globalization of qualified names } *) (** These functions globalize a (partially) qualified name or fail with @@ -95,7 +91,6 @@ val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path val locate_section : qualid -> DirPath.t -val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message @@ -109,7 +104,6 @@ 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 @@ -125,7 +119,6 @@ val exists_modtype : full_path -> bool 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 } *) @@ -144,7 +137,6 @@ val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_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 *) @@ -166,7 +158,6 @@ 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 (** Deprecated synonyms *) -- cgit v1.2.3