Module `Ssreflect_plugin.Ssripats`

type ssriop = | IOpId of Names.Id.t | IOpDrop | IOpTemporay | IOpInaccessible of string option | IOpInaccessibleAll | IOpAbstractVars of Names.Id.t list | IOpFastNondep | IOpInj of ssriops list | IOpDispatchBlock of Ssrast.id_block | IOpDispatchBranches of ssriops list | IOpCaseBlock of Ssrast.id_block | IOpCaseBranches of ssriops list | IOpRewrite of Ssrast.ssrocc * Ssrast.ssrdir | IOpView of Ssrast.ssrclear option * Ssrast.ssrview | IOpClear of Ssrast.ssrclear * Ssrast.ssrhyp option | IOpSimpl of Ssrast.ssrsimpl | IOpEqGen of unit Proofview.tactic | IOpNoop
and ssriops = ssriop list

val tclCompileIPats : Ssrast.ssripats -> ssriops
val tclIPAT : ssriops -> unit Proofview.tactic
val tclIPATssr : Ssrast.ssripats -> unit Proofview.tactic
val ssrmovetac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
val ssrelimtac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
val ssrcasetac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic
val ssrabstract : Ssrast.ssrdgens -> unit Proofview.tactic

module Internal : sig ... end