Module Ltac_plugin.Tacenv

Tactic naming
val push_tactic : Nametab.visibility -> Libnames.full_path -> Tacexpr.ltac_constant -> unit
val locate_tactic : Libnames.qualid -> Tacexpr.ltac_constant
val locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant list
val exists_tactic : Libnames.full_path -> bool
val path_of_tactic : Tacexpr.ltac_constant -> Libnames.full_path
val shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid
Tactic notations
type alias = Names.KerName.t

Type of tactic alias, used in the TacAlias node.

type alias_tactic = {
alias_args : Names.Id.t list;
alias_body : Tacexpr.glob_tactic_expr;
alias_deprecation : Deprecation.t option;
}

Contents of a tactic notation

val register_alias : alias -> alias_tactic -> unit

Register a tactic alias.

val interp_alias : alias -> alias_tactic

Recover the body of an alias. Raises an anomaly if it does not exist.

val check_alias : alias -> bool

Returns true if an alias is defined, false otherwise.

Coq tactic definitions
val register_ltac : bool -> bool -> ?⁠deprecation:Deprecation.t -> Names.Id.t -> Tacexpr.glob_tactic_expr -> unit

Register a new Ltac with the given name and body.

The first boolean indicates whether this is done from ML side, rather than Coq side. If the second boolean flag is set to true, then this is a local definition. It also puts the Ltac name in the nametab, so that it can be used unqualified.

val redefine_ltac : bool -> ?⁠deprecation:Deprecation.t -> Names.KerName.t -> Tacexpr.glob_tactic_expr -> unit

Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition.

val interp_ltac : Names.KerName.t -> Tacexpr.glob_tactic_expr

Find a user-defined tactic by name. Raise Not_found if it is absent.

val is_ltac_for_ml_tactic : Names.KerName.t -> bool

Whether the tactic is defined from ML-side

val tac_deprecation : Names.KerName.t -> Deprecation.t option

The tactic deprecation notice, if any

type ltac_entry = {
tac_for_ml : bool;

Whether the tactic is defined from ML-side

tac_body : Tacexpr.glob_tactic_expr;

The current body of the tactic

tac_redef : Names.ModPath.t list;

List of modules redefining the tactic in reverse chronological order

tac_deprecation : Deprecation.t option;

Deprecation notice to be printed when the tactic is used

}
val ltac_entries : unit -> ltac_entry Names.KNmap.t

Low-level access to all Ltac entries currently defined.

ML tactic extensions
type ml_tactic = Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic

Type of external tactics, used by TacML.

val register_ml_tactic : ?⁠overwrite:bool -> Tacexpr.ml_tactic_name -> ml_tactic array -> unit

Register an external tactic.

val interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic

Get the named tactic. Raises a user error if it does not exist.