Ssrequality (rocq-runtime.Ssreflect

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