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

6 files changed, 17 insertions, 15 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index acb297ddf..47a59ba63 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -28,7 +28,7 @@ let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index 5529ea700..f10f98e23 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -26,7 +26,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index ad8b54d4d..e158e0b51 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -16,11 +16,12 @@ let () = Mltop.add_known_module __coq_plugin_name
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
+open Pp
+open CErrors
+open Names
 open Glob_term
 open Bigint
 open Coqlib
-open Pp
-open CErrors
 (*i*)
 
 (**********************************************************************)
@@ -61,10 +62,10 @@ exception Non_closed_number
 let rec int_of_nat x = DAst.with_val (function
   | GApp (r, [a]) ->
     begin match DAst.get r with
-    | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+    | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a)
     | _ -> raise Non_closed_number
     end
-  | GRef (z,_) when Globnames.eq_gr z glob_O -> zero
+  | GRef (z,_) when GlobRef.equal z glob_O -> zero
   | _ -> raise Non_closed_number
   ) x
 
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 372e8ff30..94aa14335 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -30,7 +30,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let positive_path = make_path binnums "positive"
@@ -66,7 +66,7 @@ let pos_of_bignat ?loc x =
 let rec bignat_of_pos c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
   | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -98,7 +98,7 @@ let z_of_int ?loc n =
 let bigint_of_z c = match DAst.get c with
   | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
   | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 2421cc12f..c22869f4d 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open Globnames
 open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
@@ -34,7 +35,7 @@ let glob_String = lazy (make_reference "String")
 let glob_EmptyString = lazy (make_reference "EmptyString")
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 open Lazy
@@ -55,7 +56,7 @@ let uninterp_string (AnyGlobConstr r) =
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | GRef (z,_) when eq_gr z (force glob_EmptyString) ->
+    | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index d5300e474..09fe8bf70 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -71,13 +71,13 @@ let interp_positive ?loc n =
 (**********************************************************************)
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let rec bignat_of_pos x = DAst.with_val (function
   | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
   | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
+  | GRef (a, _)                when GlobRef.equal a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
   ) x
 
@@ -132,7 +132,7 @@ let n_of_int ?loc n =
 
 let bignat_of_n n = DAst.with_val (function
   | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
-  | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+  | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
   ) n
 
@@ -180,7 +180,7 @@ let z_of_int ?loc n =
 let bigint_of_z z = DAst.with_val (function
   | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
   | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
   ) z