Module Autorewrite

This files implements the autorewrite tactic.

type raw_rew_rule = (Constr.constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t

Rewriting rules before tactic interpretation

val add_rew_rules : string -> raw_rew_rule list -> unit

To add rewriting rules to a base

val autorewrite : ?⁠conds:Equality.conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic

The AutoRewrite tactic. The optional conditions tell rewrite how to handle matching and side-condition solving. Default is Naive: first match in the clause, don't look at the side-conditions to tell if the rewrite succeeded.

val autorewrite_in : ?⁠conds:Equality.conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic
type rew_rule = {
rew_lemma : Constr.constr;
rew_type : Constr.types;
rew_pat : Constr.constr;
rew_ctx : Univ.ContextSet.t;
rew_l2r : bool;
rew_tac : Genarg.glob_generic_argument option;
}

Rewriting rules

val find_rewrites : string -> rew_rule list
val find_matches : string -> Constr.constr -> rew_rule list
val auto_multi_rewrite : ?⁠conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tactic
val auto_multi_rewrite_with : ?⁠conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
val print_rewrite_hintdb : string -> Pp.t
type hypinfo = {
hyp_cl : Clenv.clausenv;
hyp_prf : Constr.constr;
hyp_ty : Constr.types;
hyp_car : Constr.constr;
hyp_rel : Constr.constr;
hyp_l2r : bool;
hyp_left : Constr.constr;
hyp_right : Constr.constr;
}
val find_applied_relation : ?⁠loc:Loc.t -> bool -> Environ.env -> Evd.evar_map -> Constr.constr -> bool -> hypinfo