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 :
locality:Hints.hint_locality ->
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
module RewRule : sig ... end
Rewriting rules
val find_rewrites : string -> RewRule.t list
val find_matches : Environ.env -> string -> Constr.constr -> RewRule.t 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
val default_hint_rewrite_locality : unit -> Hints.hint_locality