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