diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 14:06:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 18:59:00 +0200 |
| commit | 1a6a26d29252da54b86bf663a66ddd909905d1cb (patch) | |
| tree | 2489daca9a966cf869025a535f98f5799ff13ceb /library/nametab.mli | |
| parent | 2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff) | |
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.
Diffstat (limited to 'library/nametab.mli')
| -rw-r--r-- | library/nametab.mli | 9 |
1 files changed, 0 insertions, 9 deletions
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 *) |