Module `Elim`

val case_tac : bool -> Tactypes.or_and_intro_pattern option -> (Tactypes.intro_patterns -> EConstr.named_context -> unit Proofview.tactic) -> EConstr.constr -> (Names.inductive * EConstr.EInstance.t * EConstr.t array) -> Names.Id.t -> 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