diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-26 11:46:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-26 11:46:59 +0000 |
| commit | 446155d07c89e148ec61bb0c414f4cd8a73311e0 (patch) | |
| tree | 6e7bfa33c9cf4422ab97444aab287a18def92e2e /pretyping/termops.mli | |
| parent | 91c9a1294d236f55ff6fecdf1d763e7185590ea1 (diff) | |
Adding subst_term up to conv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index c6ca30407..c74551735 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -153,6 +153,13 @@ val no_occurrences_in_set : occurrences val subst_term_occ_gen : occurrences -> int -> constr -> types -> int * types +(** [subst_term_occ_gen_modulo] looks for subterm modulo a comparison + function returning a substitution of type ['a]; a function for + merging substitution and an initial substitution are required too *) +val subst_term_occ_gen_modulo : + occurrences -> (constr -> constr -> 'a) -> ('a -> 'a -> 'a) -> 'a -> + int -> constr -> types -> 'a * int * types + (** [subst_term_occ occl c d] replaces occurrences of [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC) *) val subst_term_occ : occurrences -> constr -> constr -> constr |