From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 14 Nov 2017 22:36:47 +0100
Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel
 style.

In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.

This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.

A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
---
 pretyping/typeclasses.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e73a78fb84..4386144fe2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -71,10 +71,10 @@ type typeclass = {
   cl_univs : Univ.AUContext.t;
 
   (* The class implementation *)
-  cl_impl : global_reference;
+  cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : global_reference option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
@@ -91,12 +91,12 @@ type typeclass = {
 type typeclasses = typeclass Refmap.t
 
 type instance = {
-  is_class: global_reference;
+  is_class: GlobRef.t;
   is_info: hint_info_expr;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
-  is_impl: global_reference;
+  is_impl: GlobRef.t;
 }
 
 type instances = (instance Refmap.t) Refmap.t
@@ -480,7 +480,7 @@ let instances r =
   let cl = class_info r in instances_of cl    
 
 let is_class gr = 
-  Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes
+  Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
 let is_instance = function
   | ConstRef c ->
-- 
cgit v1.2.3