ElimEliminations tactics.
val case_tac :
bool ->
Tactypes.or_and_intro_pattern option ->
( Tactypes.intro_patterns -> EConstr.named_context -> unit Proofview.tactic ) ->
(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