[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, 4 insertions, 4 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3f2792518..ae1065ef5 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -561,7 +561,7 @@ let declare_mutual_definition l =
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
-    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+    let kn = match gr with GlobRef.ConstRef kn -> kn | _ -> assert false in
     Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
     List.iter progmap_remove l; kn
 
@@ -744,7 +744,7 @@ let all_programs () =
 type progress =
     | Remain of int
     | Dependent
-    | Defined of global_reference
+    | Defined of GlobRef.t
 
 let obligations_message rem =
   if rem > 0 then
@@ -770,7 +770,7 @@ let update_obls prg obls rem =
 	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
 	    if List.for_all (fun x -> obligations_solved x) progs then
 	      let kn = declare_mutual_definition progs in
-		Defined (ConstRef kn)
+                Defined (GlobRef.ConstRef kn)
 	    else Dependent)
 
 let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
@@ -891,7 +891,7 @@ let obligation_terminator name num guard hook auto pf =
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in
-  let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+  let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
   let () = match obl.obl_status with
       (true, Evar_kinds.Expand)