diff options
Diffstat (limited to 'plugins/ltac/tacentries.mli')
| -rw-r--r-- | plugins/ltac/tacentries.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index aa8f4efe6..ab2c6b307 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -62,3 +62,6 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) + +val print_located_tactic : Libnames.reference -> unit +(** Display the absolute name of a tactic. *) |