diff options
Diffstat (limited to 'plugins/ltac/tacenv.mli')
| -rw-r--r-- | plugins/ltac/tacenv.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 958109e5a..4ecc978fe 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -7,11 +7,21 @@ (************************************************************************) open Names +open Libnames open Tacexpr open Geninterp (** This module centralizes the various ways of registering tactics. *) +(** {5 Tactic naming} *) + +val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit +val locate_tactic : qualid -> ltac_constant +val locate_extended_all_tactic : qualid -> ltac_constant list +val exists_tactic : full_path -> bool +val path_of_tactic : ltac_constant -> full_path +val shortest_qualid_of_tactic : ltac_constant -> qualid + (** {5 Tactic notations} *) type alias = KerName.t |