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