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.