[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.

1 files changed, 23 insertions, 15 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index 96e020aed..566fcd0f9 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -500,21 +500,6 @@ val constructor_user_hash : constructor -> int
 val constructor_syntactic_ord : constructor -> constructor -> int
 val constructor_syntactic_hash : constructor -> int
 
-(** {6 Global reference is a kernel side type for all references together } *)
-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 required in grammar.cma *)
-type evaluable_global_reference =
-  | EvalVarRef of Id.t
-  | EvalConstRef of Constant.t
-
-val eq_egr : evaluable_global_reference ->  evaluable_global_reference
-  -> bool
-
 (** {6 Hash-consing } *)
 
 val hcons_con : Constant.t -> Constant.t
@@ -749,6 +734,29 @@ end
 type projection = Projection.t
 [@@ocaml.deprecated "Alias for [Projection.t]"]
 
+(** {6 Global reference is a kernel side type for all references together } *)
+
+(* XXX: Should we define GlobRefCan GlobRefUser? *)
+module GlobRef : sig
+
+  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. *)
+
+  val equal : t -> t -> bool
+
+end
+
+(** Better to have it here that in Closure, since required in grammar.cma *)
+(* XXX: Move to a module *)
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
+
 val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
 [@@ocaml.deprecated "Same as [Constant.make]"]