Module `Elim`

Eliminations tactics.

val introCaseAssumsThen : Tactics.evars_flag -> (Tactypes.intro_patterns -> Tacticals.branch_assumptions -> unit Proofview.tactic) -> Tacticals.branch_args -> unit Proofview.tactic
val h_decompose : Names.inductive list -> EConstr.constr -> unit Proofview.tactic
val h_decompose_or : EConstr.constr -> unit Proofview.tactic
val h_decompose_and : EConstr.constr -> unit Proofview.tactic
val h_double_induction : Tactypes.quantified_hypothesis -> Tactypes.quantified_hypothesis -> unit Proofview.tactic