Ssrequality (coq-core.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