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.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index a65b8275e6..a5c179bf78 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1066,19 +1066,9 @@ let global_of_constr sigma c =
   | Var id -> VarRef id, EConstr.EInstance.empty
   | _ -> raise Not_found
 
-let is_global sigma c t =
-  let open GlobRef in
-  match c, EConstr.kind sigma t with
-  | ConstRef c, Const (c', _) -> Constant.equal c c'
-  | IndRef i, Ind (i', _) -> eq_ind i i'
-  | ConstructRef i, Construct (i', _) -> eq_constructor i i'
-  | VarRef id, Var id' -> Id.equal id id'
-  | _ -> false
+let is_global = EConstr.isRefX
 
-let isGlobalRef sigma c =
-  match EConstr.kind sigma c with
-  | Const _ | Ind _ | Construct _ | Var _ -> true
-  | _ -> false
+let isGlobalRef = EConstr.isRef
 
 let is_template_polymorphic_ind env sigma f =
   match EConstr.kind sigma f with
-- 
cgit v1.2.3