diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-30 18:46:00 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-30 18:46:00 +0000 |
| commit | fa7e44d2b1a71fd8662ee720efdde2295679975b (patch) | |
| tree | 2df28cd5b608f0a6cfc1cc3689dbaa885d5673bb /tactics/autorewrite.mli | |
| parent | f8e2c78e8bfd8679a77e3cf676bde58c4efffd45 (diff) | |
Add new variants of [rewrite] and [autorewrite] which differ in the
selection of occurrences.
We use a new function [unify_to_subterm_all] to return all occurrences
of a lemma and produce the rewrite depending on a new [conditions] option
that controls if we must rewrite one or all occurrences and if the side
conditions should be solved or not for a single rewrite to be successful.
[rewrite*] will rewrite the first occurrence whose side-conditions are
solved while [autorewrite*] will rewrite all occurrences whose
side-conditions are solved.
Not supported by [setoid_rewrite] yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index c8b3410dc..17777084d 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,6 +12,7 @@ open Term open Tacexpr open Tacmach +open Equality (*i*) (* Rewriting rules before tactic interpretation *) @@ -20,9 +21,12 @@ type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr (* To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit -(* The AutoRewrite tactic *) -val autorewrite : tactic -> string list -> tactic -val autorewrite_in : Names.identifier -> tactic -> string list -> 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 : ?conds:conditions -> tactic -> string list -> tactic +val autorewrite_in : ?conds:conditions -> Names.identifier -> tactic -> string list -> tactic (* Rewriting rules *) type rew_rule = { rew_lemma: constr; @@ -35,9 +39,9 @@ val find_rewrites : string -> rew_rule list val find_matches : string -> constr -> rew_rule list -val auto_multi_rewrite : string list -> Tacticals.clause -> tactic +val auto_multi_rewrite : ?conds:conditions -> string list -> Tacticals.clause -> tactic -val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic +val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Tacticals.clause -> tactic val print_rewrite_hintdb : string -> unit |