diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /pretyping/find_subterm.mli | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'pretyping/find_subterm.mli')
| -rw-r--r-- | pretyping/find_subterm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 1ddae01e2b..c71cb207ab 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -43,13 +43,13 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function matching subterms at the indicated occurrences [occl] with [mk ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) -val replace_term_occ_modulo : evar_map -> occurrences or_like_first -> +val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first -> 'a testing_function -> (unit -> constr) -> constr -> constr (** [replace_term_occ_decl_modulo] is similar to [replace_term_occ_modulo] but for a named_declaration. *) val replace_term_occ_decl_modulo : - evar_map -> + env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> 'a testing_function -> (unit -> constr) -> named_declaration -> named_declaration |