package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid
type alias = Names.KerName.t
type alias_tactic = {
  1. alias_args : Names.Id.t list;
  2. alias_body : Tacexpr.glob_tactic_expr;
  3. alias_deprecation : Vernacinterp.deprecation option;
}
val register_alias : alias -> alias_tactic -> unit
val interp_alias : alias -> alias_tactic
val check_alias : alias -> bool
val register_ltac : bool -> bool -> ?deprecation:Vernacinterp.deprecation -> Names.Id.t -> Tacexpr.glob_tactic_expr -> unit
val redefine_ltac : bool -> ?deprecation:Vernacinterp.deprecation -> Names.KerName.t -> Tacexpr.glob_tactic_expr -> unit
val is_ltac_for_ml_tactic : Names.KerName.t -> bool
val tac_deprecation : Names.KerName.t -> Vernacinterp.deprecation option
type ltac_entry = {
  1. tac_for_ml : bool;
  2. tac_body : Tacexpr.glob_tactic_expr;
  3. tac_redef : Names.ModPath.t list;
  4. tac_deprecation : Vernacinterp.deprecation option;
}
val ltac_entries : unit -> ltac_entry Names.KNmap.t
type ml_tactic = Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic
val register_ml_tactic : ?overwrite:bool -> Tacexpr.ml_tactic_name -> ml_tactic array -> unit
val interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic