From a5f9b0ea89c9a595ce47c549a2ebb976b0ac3aa2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Feb 2020 14:01:56 +0100
Subject: Standardize constr -> globref operations to use destRef/isRef/isRefX

Instead of various termops and globnames aliases.
---
 engine/termops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/termops.mli')

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
 
-- 
cgit v1.2.3