diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 11:09:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 21:05:06 +0200 |
| commit | c955779074833066e9db81c9fb1b32493cfebfa2 (patch) | |
| tree | b5268515c605ea0336b0233e5d751ab57311bc15 /pretyping/find_subterm.mli | |
| parent | 9ec08ac299faf6acdfd6061fd21a00e3446aec79 (diff) | |
Make eq_pattern_test/eq_test work up to the equivalence of primitive
projections with their eta-expanded constant form.
Diffstat (limited to 'pretyping/find_subterm.mli')
| -rw-r--r-- | pretyping/find_subterm.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 44e435e69..b24c95807 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -12,6 +12,7 @@ open Context open Term open Evd open Pretype_errors +open Environ (** Finding subterms, possibly up to some unification function, possibly at some given occurrences *) @@ -34,7 +35,7 @@ type 'a testing_function = { (** This is the basic testing function, looking for exact matches of a closed term *) -val make_eq_univs_test : evar_map -> constr -> evar_map testing_function +val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function (** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm modulo a testing function [test] and replaces successfully @@ -53,12 +54,12 @@ val replace_term_occ_decl_modulo : (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), unifying universes which results in a set of constraints. *) -val subst_closed_term_occ : evar_map -> occurrences -> constr -> +val subst_closed_term_occ : env -> evar_map -> occurrences -> constr -> constr -> constr * evar_map (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [decl]. *) -val subst_closed_term_occ_decl : evar_map -> +val subst_closed_term_occ_decl : env -> evar_map -> occurrences * hyp_location_flag -> constr -> named_declaration -> named_declaration * evar_map |