aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.mli
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-31 10:59:24 +0200
committerMaxime Dénès2018-05-31 10:59:24 +0200
commitac8a84e3b4dc530b000e17b72c7e26f7a957420f (patch)
treebaf58d74b6629034cecb577eade044f29313cc4d /engine/termops.mli
parent22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (diff)
parent0dc79e09b2b7c369b35191191aa257451a536540 (diff)
Merge PR #6969: [api] Remove functions deprecated in 8.8
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index e2ddcd36e7..bb3cbb6a82 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -113,8 +113,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