diff options
Diffstat (limited to 'pretyping/find_subterm.mli')
| -rw-r--r-- | pretyping/find_subterm.mli | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index b24c958074..ea1ce6228b 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -26,11 +26,12 @@ exception SubtermUnificationError of subterm_unification_error function to merge substitutions and an initial substitution; last_found is used for error messages and it has to be initialized with None. *) + type 'a testing_function = { match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option + mutable last_found : position_reporting option } (** This is the basic testing function, looking for exact matches of a @@ -42,25 +43,26 @@ 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 : - occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr +val replace_term_occ_modulo : 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 : - occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) -> + (occurrences * hyp_location_flag) or_like_first -> + 'a testing_function -> (unit -> constr) -> named_declaration -> named_declaration (** [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 : env -> evar_map -> occurrences -> constr -> - constr -> constr * evar_map +val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> + 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 : env -> evar_map -> - occurrences * hyp_location_flag -> + (occurrences * hyp_location_flag) or_like_first -> constr -> named_declaration -> named_declaration * evar_map (** Miscellaneous *) |