diff options
| author | msozeau | 2009-06-30 18:46:00 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-30 18:46:00 +0000 |
| commit | fa7e44d2b1a71fd8662ee720efdde2295679975b (patch) | |
| tree | 2df28cd5b608f0a6cfc1cc3689dbaa885d5673bb /tactics/equality.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/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 36 |
1 files changed, 23 insertions, 13 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index bcbe3e222d..deb68aac8f 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -27,36 +27,46 @@ open Rawterm open Genarg (*i*) +type orientation = bool + +type conditions = + | Naive (* Only try the first occurence of the lemma (default) *) + | FirstSolved (* Use the first match whose side-conditions are solved *) + | AllMatches (* Rewrite all matches whose side-conditions are solved *) + val general_rewrite_bindings : - bool -> occurrences -> constr with_bindings -> evars_flag -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic val general_rewrite : - bool -> occurrences -> constr -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> constr -> tactic (* Equivalent to [general_rewrite l2r] *) -val rewriteLR : constr -> tactic -val rewriteRL : constr -> tactic +val rewriteLR : ?tac:(tactic * conditions) -> constr -> tactic +val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) val register_general_setoid_rewrite_clause : - (identifier option -> bool -> + (identifier option -> orientation -> occurrences -> open_constr -> new_goals:constr list -> tactic) -> unit val register_is_applied_setoid_relation : (constr -> bool) -> unit -val general_rewrite_bindings_in : - bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic +val general_rewrite_ebindings_clause : identifier option -> + orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic + +val general_rewrite_bindings_in : + orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : - bool -> occurrences -> identifier -> constr -> evars_flag -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic -val general_multi_rewrite : - bool -> evars_flag -> open_constr with_bindings -> clause -> tactic +val general_multi_rewrite : + orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic val general_multi_multi_rewrite : evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> - tactic option -> tactic + (tactic * conditions) option -> tactic -val conditional_rewrite : bool -> tactic -> open_constr with_bindings -> tactic +val conditional_rewrite : orientation -> tactic -> open_constr with_bindings -> tactic val conditional_rewrite_in : - bool -> identifier -> tactic -> open_constr with_bindings -> tactic + orientation -> identifier -> tactic -> open_constr with_bindings -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic |