aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index f970b9ece0..7bbf87239d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -264,10 +264,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
val is_section_variable : Id.t -> bool
val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t
+[@@ocaml.deprecated "Use [EConstr.destRef] instead (throws DestKO instead of Not_found)."]
val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
val isGlobalRef : Evd.evar_map -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRef] instead."]
val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool