Coretactics (coq-core.Ltac_plugin.Coretactics)

val simple_induct : Tactypes.quantified_hypothesis -> unit Proofview.tactic

val simple_destruct : Tactypes.quantified_hypothesis -> unit Proofview.tactic

val initial_atomic : unit -> unit

val initial_name : string -> Tacexpr.ml_tactic_name

val initial_entry : string -> Tacexpr.ml_tactic_entry

val register_list_tactical : string -> (unit Proofview.tactic list -> unit Proofview.tactic) -> unit

val initial_tacticals : unit -> unit