diff options
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index e2ddcd36e7..2554940314 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -75,8 +75,9 @@ val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val fold_constr_with_full_binders : Evd.evar_map -> - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b + (rel_declaration -> 'a -> 'a) -> + ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> @@ -94,6 +95,7 @@ exception Occur val occur_meta : Evd.evar_map -> constr -> bool val occur_existential : Evd.evar_map -> constr -> bool val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : @@ -113,8 +115,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t -val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) -[@@ocaml.deprecated "alias of Termops.dependent"] (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list |