Ssreflect_plugin.Ssrelimtype elim_what = | EConstr of Ssrast.ssrhyp list
* Ssrmatching_plugin.Ssrmatching.occ
* EConstr.constr |
| EGen of (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ)
* Ssrmatching_plugin.Ssrmatching.cpattern |
val ssrelim :
?is_case:bool ->
((Ssrast.ssrhyps option * Ssrast.ssrocc)
* Ssrmatching_plugin.Ssrmatching.cpattern)
list ->
elim_what ->
?elim:EConstr.constr ->
Ssrast.ssripat option ->
( ?seed:Names.Name.t list array ->
elim_what ->
Ssrast.ssripat option ->
unit Proofview.tactic ->
bool ->
Ssrast.ssrhyp list ->
unit Proofview.tactic ) ->
unit Proofview.tacticval elimtac : EConstr.constr -> unit Proofview.tacticval casetac :
EConstr.constr ->
( ?seed:Names.Name.t list array ->
unit Proofview.tactic ->
unit Proofview.tactic ) ->
unit Proofview.tacticval is_injection_case : Environ.env -> Evd.evar_map -> EConstr.t -> boolval perform_injection : EConstr.constr -> unit Proofview.tacticval ssrscase_or_inj_tac : EConstr.constr -> unit Proofview.tactic