AutorewriteThis files implements the autorewrite tactic.
type raw_rew_rule = (Constr.constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.tRewriting rules before tactic interpretation
val add_rew_rules : locality:Hints.hint_locality -> string -> raw_rew_rule list -> unitTo add rewriting rules to a base
val autorewrite : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> unit Proofview.tacticThe 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.tacticmodule RewRule : sig ... endRewriting rules
val find_rewrites : string -> RewRule.t listval find_matches : string -> Constr.constr -> RewRule.t listval auto_multi_rewrite : ?conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tacticval auto_multi_rewrite_with : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tacticval print_rewrite_hintdb : string -> Pp.tval default_hint_rewrite_locality : unit -> Hints.hint_locality