Rewrite (rocq-runtime.Rewrite)

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

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

type rewrite_result_info = {

rew_rel : EConstr.constr;

rew_to : EConstr.constr;

rew_prf : EConstr.constr;

}

type rewrite_result =

| Fail

| Identity

| Success of rewrite_result_info

val subst_rewrite_result : Evd.evar_map -> (Names.Id.t -> EConstr.constr) -> rewrite_result -> rewrite_result

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