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/eConstr.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 90f50b764c..181714460d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -152,6 +152,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types
 val isRel  : Evd.evar_map -> t -> bool
 val isVar  : Evd.evar_map -> t -> bool
 val isInd  : Evd.evar_map -> t -> bool
+val isRef : Evd.evar_map -> t -> bool
 val isEvar : Evd.evar_map -> t -> bool
 val isMeta : Evd.evar_map -> t -> bool
 val isSort : Evd.evar_map -> t -> bool
@@ -175,6 +176,7 @@ val isArity : Evd.evar_map -> t -> bool
 
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
 val isRelN : Evd.evar_map -> int -> t -> bool
+val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool
 
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
@@ -319,6 +321,7 @@ val fresh_global :
   Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
 
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
 (** {5 Extra} *)
 
-- 
cgit v1.2.3