diff options
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index e2ddcd36e..6e63539ca 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -94,6 +94,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 +114,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 |