Module Ltac_plugin.RewriteSource

TODO: document and clean me!

Sourcetype rewrite_attributes
Sourcetype unary_strategy =
  1. | Subterms
  2. | Subterm
  3. | Innermost
  4. | Outermost
  5. | Bottomup
  6. | Topdown
  7. | Progress
  8. | Try
  9. | Any
  10. | Repeat
Sourcetype binary_strategy =
  1. | Compose
  2. | Choice
Sourcetype ('constr, 'redexpr) strategy_ast =
  1. | StratId
  2. | StratFail
  3. | StratRefl
  4. | StratUnary of unary_strategy * ('constr, 'redexpr) strategy_ast
  5. | StratBinary of binary_strategy * ('constr, 'redexpr) strategy_ast * ('constr, 'redexpr) strategy_ast
  6. | StratConstr of 'constr * bool
  7. | StratTerms of 'constr list
  8. | StratHints of bool * string
  9. | StratEval of 'redexpr
  10. | StratFold of 'constr
Sourcetype rewrite_proof =
  1. | RewPrf of EConstr.constr * EConstr.constr
  2. | RewCast of Constr.cast_kind
Sourcetype rewrite_result_info = {
  1. rew_car : EConstr.constr;
  2. rew_from : EConstr.constr;
  3. rew_to : EConstr.constr;
  4. rew_prf : rewrite_proof;
  5. rew_evars : evars;
}
Sourcetype rewrite_result =
  1. | Fail
  2. | Identity
  3. | Success of rewrite_result_info
Sourcetype strategy
Sourceval map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
Sourceval pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('a, 'b) strategy_ast -> Pp.t
Sourceval cl_rewrite_clause_strat : strategy -> Names.Id.t option -> unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Entry point for user-level "setoid_rewrite"

Sourceval is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
Sourceval add_morphism_as_parameter : rewrite_attributes -> Constrexpr.constr_expr -> Names.Id.t -> unit
Sourceval default_morphism : ((EConstr.types * EConstr.constr option) option list * (EConstr.types * EConstr.types option) option) -> EConstr.constr -> EConstr.constr * EConstr.constr
Sourceval setoid_symmetry : unit Proofview.tactic
Sourceval setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic
Sourceval setoid_reflexivity : unit Proofview.tactic
Sourceval setoid_transitivity : EConstr.constr option -> unit Proofview.tactic