Ssrequality (p.coq.8.16.0.doc.ssreflect_plugin.Ssreflect

Sourcetype ssrwkind =

| RWred of Ssrast.ssrsimpl
| RWdef
| RWeq

Sourcetype ssrrule = ssrwkind * Ssrast.ssrterm

type ssrrwarg =
  (Ssrast.ssrdir * Ssrast.ssrmult)
  * ((Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.rpattern option)
     * ssrrule)

Sourceval dir_org : Ssrast.ssrdir -> int

Sourceval notimes : int

Sourceval nomult : Ssrast.ssrmult

Sourceval mkocc : Ssrast.ssrocc -> Ssrast.ssrdocc

Sourceval mkclr : Ssrast.ssrclear -> Ssrast.ssrdocc

Sourceval nodocc : Ssrast.ssrdocc

Sourceval noclr : Ssrast.ssrdocc

Sourceval simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic

Source

val newssrcongrtac : 
  (int * Ssrast.ssrterm) ->
  Ltac_plugin.Tacinterp.interp_sign ->
  unit Proofview.tactic

Source

val mk_rwarg : 
  (Ssrast.ssrdir * (int * Ssrast.ssrmmod)) ->
  ((Ssrast.ssrclear option * Ssrast.ssrocc)
   * Ssrmatching_plugin.Ssrmatching.rpattern option) ->
  (ssrwkind * Ssrast.ssrterm) ->
  ssrrwarg

Sourceval norwmult : Ssrast.ssrdir * Ssrast.ssrmult

Source

val norwocc : 
  (Ssrast.ssrclear option * Ssrast.ssrocc)
  * Ssrmatching_plugin.Ssrmatching.rpattern option

Source

val ssr_is_setoid : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  EConstr.t array ->
  bool

Source

val ssrinstancesofrule : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Ssrast.ssrdir ->
  Ssrast.ssrterm ->
  unit Proofview.tactic

Source

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

Source

val ipat_rewrite : 
  Ssrast.ssrocc ->
  Ssrast.ssrdir ->
  EConstr.t ->
  unit Proofview.tactic

Source

val unlocktac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  (Ssrmatching_plugin.Ssrmatching.occ * Ssrast.ssrterm) list ->
  unit Proofview.tactic