Ltac_plugin.TacenvThis module centralizes the various ways of registering tactics.
val push_tactic : Nametab.visibility -> Libnames.full_path -> Tacexpr.ltac_constant -> unitval locate_tactic : Libnames.qualid -> Tacexpr.ltac_constantval locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant listval exists_tactic : Libnames.full_path -> boolval path_of_tactic : Tacexpr.ltac_constant -> Libnames.full_pathval shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualidtype alias = Names.KerName.tType 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 -> unitRegister a tactic alias.
val interp_alias : alias -> alias_tacticRecover the body of an alias. Raises an anomaly if it does not exist.
val check_alias : alias -> boolReturns true if an alias is defined, false otherwise.
val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Names.Id.t -> Tacexpr.glob_tactic_expr -> unitRegister 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 -> unitReplace 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_exprFind a user-defined tactic by name. Raise Not_found if it is absent.
val is_ltac_for_ml_tactic : Names.KerName.t -> boolWhether the tactic is defined from ML-side
val tac_deprecation : Names.KerName.t -> Deprecation.t optionThe 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.tLow-level access to all Ltac entries currently defined.
type ml_tactic = Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tacticType of external tactics, used by TacML.
val register_ml_tactic : ?overwrite:bool -> Tacexpr.ml_tactic_name -> ml_tactic array -> unitRegister an external tactic.
val interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tacticGet the named tactic. Raises a user error if it does not exist.