Rewrite (rocq-runtime.Rewrite)

exception RewriteFailure of Environ.env * Evd.evar_map * Pretype_errors.pretype_error

type evars = Evd.evar_map * Evar.Set.t

module Result : sig ... end

type strategy

val cl_rewrite_clause_strat : 
  strategy ->
  Names.Id.t option ->
  unit Proofview.tactic

Entry point for user-level "rewrite_strat"

val cl_rewrite_clause : 
  EConstr.t Tactypes.with_bindings Tactypes.delayed_open ->
  bool ->
  Locus.occurrences ->
  Names.Id.t option ->
  unit Proofview.tactic

Entry point for user-level "setoid_rewrite"

val is_applied_rewrite_relation : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  EConstr.constr ->
  EConstr.types option

val get_reflexive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val get_symmetric_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val get_transitive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val setoid_symmetry : unit Proofview.tactic

val setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic

val setoid_reflexivity : unit Proofview.tactic

val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic

module Strategies : sig ... end

module Internal : sig ... end