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.
---
 kernel/names.ml | 44 ++++++++++++++++++++++++++++----------------
 1 file changed, 28 insertions(+), 16 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index a3aa71f24f..58d311dd58 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -701,22 +701,6 @@ end
 module Constrmap = Map.Make(ConstructorOrdered)
 module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
-type global_reference =
-  | 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. *)
-  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
-
-(* Better to have it here that in closure, since used in grammar.cma *)
-type evaluable_global_reference =
-  | EvalVarRef of Id.t
-  | EvalConstRef of Constant.t
-
-let eq_egr e1 e2 = match e1, e2 with
-    EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
-  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
-  | _, _ -> false
-
 (** {6 Hash-consing of name objects } *)
 
 module Hind = Hashcons.Make(
@@ -904,6 +888,34 @@ end
 
 type projection = Projection.t
 
+module GlobRef = struct
+
+  type 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. *)
+    | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+
+  let equal 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
+    | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
+
+end
+
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+(* Better to have it here that in closure, since used in grammar.cma *)
+let eq_egr e1 e2 = match e1, e2 with
+    EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
+  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
+  | _, _ -> false
+
 let constant_of_kn = Constant.make1
 let constant_of_kn_equiv = Constant.make
 let make_con = Constant.make3
-- 
cgit v1.2.3