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

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 150dad16c2..e37a58be61 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -119,6 +119,20 @@ let isVarId sigma id c =
 let isRelN sigma n c =
   match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
 
+let isRef sigma c = match kind sigma c with
+  | Const _ | Ind _ | Construct _ | Var _ -> true
+  | _ -> false
+
+let isRefX sigma x c =
+  let open GlobRef in
+  match x, kind sigma c 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 destRel sigma c = match kind sigma c with
 | Rel p -> p
 | _ -> raise DestKO
@@ -723,8 +737,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, t
 
-let is_global sigma gr c =
-  Globnames.is_global gr (to_constr sigma c)
+let is_global = isRefX
 
 module Unsafe =
 struct
-- 
cgit v1.2.3