Module `Ssreflect_plugin.Ssrelim`

val ssrelim : ?⁠is_case:bool -> ((Ssrast.ssrhyps option * Ssrast.ssrocc) * Ssrmatching_plugin.Ssrmatching.cpattern) list -> [< `EConstr of Ssrast.ssrhyp list * Ssrmatching_plugin.Ssrmatching.occ * EConstr.constr * 'b | `EGen of (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern ] as a -> ?⁠elim:EConstr.constr -> Ssrast.ssripat option -> (?⁠seed:Names.Name.t list array -> 'a -> Ssrast.ssripat option -> unit Proofview.tactic -> bool -> Ssrast.ssrhyp list -> unit Proofview.tactic) -> unit Proofview.tactic
val elimtac : EConstr.constr -> unit Proofview.tactic
val casetac : EConstr.constr -> (?⁠seed:Names.Name.t list array -> unit Proofview.tactic -> unit Proofview.tactic) -> unit Proofview.tactic
val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool
val perform_injection : EConstr.constr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
val ssrscase_or_inj_tac : EConstr.constr -> unit Proofview.tactic