diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 01:09:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:43 +0100 |
| commit | 8beca748d992cd08e2dd7448c8b28dadbcea4a16 (patch) | |
| tree | 2cb484e735e9a138991e4cd1e540c6de879e67f6 /pretyping/find_subterm.mli | |
| parent | e1010899051546467b790bca0409174bde824270 (diff) | |
Cleaning up interfaces.
We make mli files look to what they were looking before the move to EConstr
by opening this module.
Diffstat (limited to 'pretyping/find_subterm.mli')
| -rw-r--r-- | pretyping/find_subterm.mli | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index c7db84e3c..3d2ebb72d 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -11,11 +11,12 @@ open Term open Evd open Pretype_errors open Environ +open EConstr (** Finding subterms, possibly up to some unification function, possibly at some given occurrences *) -exception NotUnifiable of (EConstr.constr * EConstr.constr * unification_error) option +exception NotUnifiable of (constr * constr * unification_error) option exception SubtermUnificationError of subterm_unification_error @@ -26,7 +27,7 @@ exception SubtermUnificationError of subterm_unification_error with None. *) type 'a testing_function = { - match_fun : 'a -> EConstr.constr -> 'a; + match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; mutable last_found : position_reporting option @@ -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 : env -> evar_map -> EConstr.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 @@ -42,27 +43,27 @@ val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_f ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) val replace_term_occ_modulo : evar_map -> occurrences or_like_first -> - 'a testing_function -> (unit -> EConstr.constr) -> EConstr.constr -> constr + '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 -> (occurrences * hyp_location_flag) or_like_first -> - 'a testing_function -> (unit -> EConstr.constr) -> + 'a testing_function -> (unit -> constr) -> Context.Named.Declaration.t -> Context.Named.Declaration.t (** [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 or_like_first -> - EConstr.constr -> EConstr.constr -> constr * evar_map + 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) or_like_first -> - EConstr.constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map + constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map (** Miscellaneous *) val error_invalid_occurrence : int list -> 'a |