Ssreflect_plugin.Ssripatstype 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 listval tclCompileIPats : Ssrast.ssripats -> ssriopsval tclIPAT : ssriops -> unit Proofview.tacticval tclIPATssr : Ssrast.ssripats -> unit Proofview.tacticval ssrmovetac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tacticval ssrsmovetac : unit Proofview.tacticval ssrelimtac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tacticval ssrselimtoptac : unit Proofview.tacticval ssrcasetac : Ssrast.ssrdgens Ssrast.ssrmovearg -> unit Proofview.tacticval ssrscasetoptac : unit Proofview.tacticval ssrabstract : Ssrast.ssrdgens -> unit Proofview.tacticmodule Internal : sig ... end