From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 library/globnames.ml | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

(limited to 'library/globnames.ml')

diff --git a/library/globnames.ml b/library/globnames.ml
index 6c9c813e..6383a1f8 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Mod_subst
 open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
-type global_reference = Names.global_reference =
+type global_reference = GlobRef.t =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
@@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false
 let isIndRef = function IndRef _ -> true | _ -> false
 let isConstructRef = function ConstructRef _ -> true | _ -> false
 
-let eq_gr gr1 gr2 =
-  gr1 == gr2 || match gr1,gr2 with
-    | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2
-    | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
-    | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-    | VarRef v1, VarRef v2 -> Id.equal v1 v2
-    | _ -> false
-
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
@@ -95,8 +87,6 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-let reference_of_constr = global_of_constr
-
 let global_eq_gen eq_cst eq_ind eq_cons x y =
   x == y ||
   match x, y with
@@ -245,3 +235,6 @@ let pop_global_reference = function
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
+
+(* Deprecated *)
+let eq_gr = GlobRef.equal
-- 
cgit v1.2.3