Module `Ssreflect_plugin.Ssrequality`

type ssrwkind = | RWred of Ssrast.ssrsimpl | RWdef | RWeq
type ssrrule = ssrwkind * Ssrast.ssrterm
type ssrrwarg = (Ssrast.ssrdir * Ssrast.ssrmult) * ((Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.rpattern option) * ssrrule)

val dir_org : Ssrast.ssrdir -> int
val notimes : int
val nomult : Ssrast.ssrmult
val mkocc : Ssrast.ssrocc -> Ssrast.ssrdocc
val mkclr : Ssrast.ssrclear -> Ssrast.ssrdocc
val nodocc : Ssrast.ssrdocc
val noclr : Ssrast.ssrdocc
val simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic
val newssrcongrtac : (int * Ssrast.ssrterm) -> Ltac_plugin.Tacinterp.interp_sign -> unit Proofview.tactic
val mk_rwarg : (Ssrast.ssrdir * (int * Ssrast.ssrmmod)) -> ((Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching_plugin.Ssrmatching.rpattern option) -> (ssrwkind * Ssrast.ssrterm) -> ssrrwarg
val norwmult : Ssrast.ssrdir * Ssrast.ssrmult
val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching_plugin.Ssrmatching.rpattern option
val ssr_is_setoid : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool
val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> Ssrast.ssrterm -> unit Proofview.tactic
val ssrrewritetac : ?⁠under:bool -> ?⁠map_redex:(Environ.env -> Evd.evar_map -> before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) -> Ltac_plugin.Tacinterp.interp_sign -> ssrrwarg list -> unit Proofview.tactic
val ipat_rewrite : Ssrast.ssrocc -> Ssrast.ssrdir -> EConstr.t -> unit Proofview.tactic
val unlocktac : Ltac_plugin.Tacinterp.interp_sign -> (Ssrmatching_plugin.Ssrmatching.occ * Ssrast.ssrterm) list -> unit Proofview.tactic