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/tacinterp.ml | |
| 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/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0942fde83..667f5b84f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2345,7 +2345,7 @@ and interp_atomic ist gl = function Equality.general_multi_multi_rewrite ev (List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) - (Option.map (interp_tactic ist) by) + (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (Option.map (interp_intro_pattern ist gl) ids) |