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

15 files changed, 32 insertions, 38 deletions

diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 7e13f8f28..0e2b0c80e 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -30,4 +30,4 @@ val traverse :
    {!traverse} also applies. *)
 val assumptions :
   ?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
-     global_reference -> constr -> types ContextObjectMap.t
+     GlobRef.t -> constr -> types ContextObjectMap.t
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 1a6b4dcdb..5e602289b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -54,7 +54,7 @@ exception EqUnknown of string
 exception UndefinedCst of string
 exception InductiveWithProduct
 exception InductiveWithSort
-exception ParameterWithoutEquality of global_reference
+exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
@@ -635,7 +635,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                         | App (c,ca) -> (
                           match EConstr.kind sigma c with
                           | Ind (indeq, u) ->
-                              if eq_gr (IndRef indeq) Coqlib.glob_eq
+                              if GlobRef.equal (IndRef indeq) Coqlib.glob_eq
                               then
                                 Tacticals.New.tclTHEN
                                   (do_replace_bl mode bl_scheme_key ind
diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli
index 5cc783df7..11f26c7c3 100644
--- a/vernac/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
@@ -23,7 +23,7 @@ exception EqUnknown of string
 exception UndefinedCst of string
 exception InductiveWithProduct
 exception InductiveWithSort
-exception ParameterWithoutEquality of Globnames.global_reference
+exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
diff --git a/vernac/class.ml b/vernac/class.ml
index f0b01061b..06e1694f9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -37,7 +37,7 @@ type coercion_error_kind =
   | ForbiddenSourceClass of cl_typ
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
-  | NotAClass of global_reference
+  | NotAClass of GlobRef.t
 
 exception CoercionError of coercion_error_kind
 
diff --git a/vernac/class.mli b/vernac/class.mli
index 33d31fe1f..f7e837f3b 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -10,19 +10,18 @@
 
 open Names
 open Classops
-open Globnames
 
 (** Classes and coercions. *)
 
 (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
    from [src] to [tg] *)
-val try_add_new_coercion_with_target : global_reference -> local:bool -> 
+val try_add_new_coercion_with_target : GlobRef.t -> local:bool ->
   Decl_kinds.polymorphic ->
   source:cl_typ -> target:cl_typ ->  unit
 
 (** [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : global_reference -> local:bool -> 
+val try_add_new_coercion : GlobRef.t -> local:bool ->
   Decl_kinds.polymorphic -> unit
 
 (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
@@ -34,7 +33,7 @@ val try_add_new_coercion_subclass : cl_typ -> local:bool ->
 
 (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
-val try_add_new_coercion_with_source : global_reference -> local:bool -> 
+val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
   Decl_kinds.polymorphic -> source:cl_typ -> unit
 
 (** [try_add_new_identity_coercion id s src tg] enriches the
@@ -47,4 +46,4 @@ val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
 
 val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
 
-val class_of_global : global_reference -> cl_typ
+val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e6134ee5d..27d3a4669 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -30,7 +30,7 @@ val declare_instance_constant :
   hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
-  ?hook:(Globnames.global_reference -> unit) ->
+  ?hook:(GlobRef.t -> unit) ->
   Id.t -> (** name *)
   Univdecls.universe_decl ->
   bool -> (* polymorphic *)
@@ -50,7 +50,7 @@ val new_instance :
   (bool * constr_expr) option ->
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
-  ?hook:(Globnames.global_reference -> unit) ->
+  ?hook:(GlobRef.t -> unit) ->
   hint_info_expr ->
   Id.t
 
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index a2d20a1d1..2f2c7c4e2 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -11,7 +11,6 @@
 open Names
 open Constr
 open Entries
-open Globnames
 open Vernacexpr
 open Constrexpr
 open Decl_kinds
@@ -33,4 +32,4 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   types in_constant_universes_entry ->
   Universes.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
-  global_reference * Univ.Instance.t * bool
+  GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 010874e23..12973f51b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -8,17 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Decl_kinds
 open Names
+open Decl_kinds
 
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
-    Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
+    GlobRef.t Lemmas.declaration_hook -> GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
   Universes.universe_binders -> Entries.constant_universes_entry ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
-  Globnames.global_reference
+  GlobRef.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index aba5e32db..3d627d2f6 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,7 +34,7 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ad4c278e0..398f7d6d0 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,10 @@ open Decl_kinds
 
 type 'a declaration_hook
 val mk_hook :
-  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
+  (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook
 
 val call_hook :
-  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
+  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a
 
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (EConstr.types -> unit) -> unit
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) 
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index cc2cacd86..4b6165fb1 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,7 +12,6 @@ open Environ
 open Constr
 open Evd
 open Names
-open Globnames
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
@@ -49,7 +48,7 @@ type obligation_info =
 type progress = (* Resolution status of a program *)
   | Remain of int  (* n obligations remaining *)
   | Dependent (* Dependent on other definitions *)
-  | Defined of global_reference (* Defined as id *)
+  | Defined of GlobRef.t (* Defined as id *)
 
 val default_tactic : unit Proofview.tactic ref
 
diff --git a/vernac/record.mli b/vernac/record.mli
index 992da2aa5..308c9e9b9 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -11,7 +11,6 @@
 open Names
 open Vernacexpr
 open Constrexpr
-open Globnames
 
 val primitive_flag : bool ref
 
@@ -30,6 +29,6 @@ val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
   Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
-  Id.t * constr_expr option -> global_reference
+  Id.t * constr_expr option -> GlobRef.t
 
-val declare_existing_class : global_reference -> unit
+val declare_existing_class : GlobRef.t -> unit
diff --git a/vernac/search.ml b/vernac/search.ml
index a2a4fb40f..6d07187fe 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -22,8 +22,8 @@ open Nametab
 
 module NamedDecl = Context.Named.Declaration
 
-type filter_function = global_reference -> env -> constr -> bool
-type display_function = global_reference -> env -> constr -> unit
+type filter_function = GlobRef.t -> env -> constr -> bool
+type display_function = GlobRef.t -> env -> constr -> unit
 
 (* This option restricts the output of [SearchPattern ...],
 [SearchAbout ...], etc. to the names of the symbols matching the
@@ -61,7 +61,7 @@ let iter_named_context_name_type f =
   List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
 
 (* General search over hypothesis of a goal *)
-let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
+let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
   let iter_hyp idh typ = fn (VarRef idh) env typ in
   let evmap,e = Pfedit.get_goal_context glnum in
@@ -69,7 +69,7 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
   iter_named_context_name_type iter_hyp pfctxt
 
 (* General search over declarations *)
-let iter_declarations (fn : global_reference -> env -> constr -> unit) =
+let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
   let iter_obj (sp, kn) lobj = match object_tag lobj with
   | "VARIABLE" ->
@@ -117,8 +117,7 @@ module ConstrPriority = struct
 
   (* The priority is memoised here. Because of the very localised use
      of this module, it is not worth it making a convenient interface. *)
-  type t =
-    Globnames.global_reference * Environ.env * Constr.t * priority
+  type t = GlobRef.t * Environ.env * Constr.t * priority
   and priority = int
 
   module ConstrSet = CSet.Make(Constr)
diff --git a/vernac/search.mli b/vernac/search.mli
index a1fb7ed3e..0dc82c1c3 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -12,7 +12,6 @@ open Names
 open Constr
 open Environ
 open Pattern
-open Globnames
 
 (** {6 Search facilities. } *)
 
@@ -20,8 +19,8 @@ type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
-type filter_function = global_reference -> env -> constr -> bool
-type display_function = global_reference -> env -> constr -> unit
+type filter_function = GlobRef.t -> env -> constr -> bool
+type display_function = GlobRef.t -> env -> constr -> unit
 
 (** {6 Generic filter functions} *)