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 /library/library.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 'library/library.mli')
0 files changed, 0 insertions, 0 deletions