ElimEliminations tactics.
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.tacticval h_decompose : Names.inductive list -> EConstr.constr -> unit Proofview.tacticval h_decompose_or : EConstr.constr -> unit Proofview.tacticval h_decompose_and : EConstr.constr -> unit Proofview.tactic