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 /pretyping/unification.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 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0e85f8243..8d71ec4bd 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -34,6 +34,9 @@ val w_unify : val w_unify_to_subterm : env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr +val w_unify_to_subterm_all : + env -> ?flags:unify_flags -> constr * constr -> evar_defs -> (evar_defs * constr) list + val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs (* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type |