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

4 files changed, 56 insertions, 36 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 4f062d72f..bc486210d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -654,7 +654,7 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
   Univ.Instance.t -> Univ.Instance.t -> bool
 
 type constr_compare_fn = int -> constr -> constr -> bool
@@ -692,10 +692,10 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
-    Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2
+    Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
+  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2
   | Construct (c1,u1), Construct (c2,u2) ->
-    eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2
+    eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
     eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 0d464840c..b35ea6653 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -413,7 +413,7 @@ val compare_head : constr_compare_fn -> constr_compare_fn
 (** Convert a global reference applied to 2 instances. The int says
    how many arguments are given (as we can only use cumulativity for
    fully applied inductives/constructors) .*)
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
   Univ.Instance.t -> Univ.Instance.t -> bool
 
 (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
diff --git a/kernel/names.ml b/kernel/names.ml
index a3aa71f24..58d311dd5 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
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]"]