Rewrite (coq-core.Rewrite)

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

type unary_strategy =

| Subterms

| Subterm

| Innermost

| Outermost

| Bottomup

| Topdown

| Progress

| Try

| Any

| Repeat

type binary_strategy =

| Compose

type nary_strategy =

| Choice

type ('constr, 'redexpr) strategy_ast =

| StratId

| StratFail

| StratRefl

| StratUnary of unary_strategy * ( 'constr, 'redexpr ) strategy_ast

| StratBinary of binary_strategy
  * ( 'constr, 'redexpr ) strategy_ast
  * ( 'constr, 'redexpr ) strategy_ast

| StratNAry of nary_strategy * ( 'constr, 'redexpr ) strategy_ast list

| StratConstr of 'constr * bool

| StratTerms of 'constr list

| StratHints of bool * string

| StratEval of 'redexpr

| StratFold of 'constr

type rewrite_proof =

| RewPrf of EConstr.constr * EConstr.constr

| RewCast of Constr.cast_kind

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

type rewrite_result_info = {

rew_car : EConstr.constr;

rew_from : EConstr.constr;

rew_to : EConstr.constr;

rew_prf : rewrite_proof;

rew_evars : evars;

}

type rewrite_result =

| Fail

| Identity

| Success of rewrite_result_info

type strategy

val strategy_of_ast : 
  ( Glob_term.glob_constr * EConstr.constr Tactypes.delayed_open,
    Redexpr.red_expr Tactypes.delayed_open )
    strategy_ast ->
  strategy

val map_strategy : 
  ( 'a -> 'b ) ->
  ( 'c -> 'd ) ->
  ( 'a, 'c ) strategy_ast ->
  ( 'b, 'd ) strategy_ast

val pr_strategy : 
  ( 'a -> Pp.t ) ->
  ( 'b -> Pp.t ) ->
  ( 'a, 'b ) strategy_ast ->
  Pp.t

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

val apply_strategy : 
  strategy ->
  Environ.env ->
  Names.Id.Set.t ->
  EConstr.constr ->
  (bool * EConstr.constr) ->
  evars ->
  rewrite_result

module Internal : sig ... end