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

9 files changed, 49 insertions, 51 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8e50c977e..8f50b0aa2 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -22,7 +22,7 @@ open Globnames
 let dnet_depth = ref 8
 
 type term_label =
-| GRLabel of global_reference
+| GRLabel of GlobRef.t
 | ProdLabel
 | LambdaLabel
 | SortLabel
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 739f1014a..d02bab186 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -115,7 +115,7 @@ type 'a hints_path_atom_gen =
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
 
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
@@ -126,10 +126,10 @@ type 'a hints_path_gen =
   | PathEpsilon
 
 type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
 
 type hint_term =
-  | IsGlobRef of global_reference
+  | IsGlobRef of GlobRef.t
   | IsConstr of constr * Univ.ContextSet.t
 
 type 'a with_uid = {
@@ -153,7 +153,7 @@ type 'a with_metadata = {
 
 type full_hint = hint with_metadata
 
-type hint_entry = global_reference option * 
+type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
 type import_level = [ `LAX | `WARN | `STRICT ]
@@ -308,7 +308,7 @@ let instantiate_hint env sigma p =
   { p with code = { p.code with obj = code } }
 
 let hints_path_atom_eq h1 h2 = match h1, h2 with
-| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
+| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2
 | PathAny, PathAny -> true
 | _ -> false
 
@@ -365,7 +365,7 @@ let path_seq p p' =
 let rec path_derivate hp hint =
   let rec derivate_atoms hints hints' =
     match hints, hints' with
-    | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs'
+    | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs'
     | [], [] -> PathEpsilon
     | [], hints -> PathEmpty
     | grs, [] -> PathAtom (PathHints grs)
@@ -474,28 +474,28 @@ module Hint_db :
 sig
 type t
 val empty : ?name:hint_db_name -> transparent_state -> bool -> t
-val find : global_reference -> t -> search_entry
+val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
-val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
-		      (global_reference * constr array) -> constr -> t -> full_hint list
+                      (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val map_eauto : evar_map -> secvars:Id.Pred.t ->
-		(global_reference * constr array) -> constr -> t -> full_hint list
+                (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val map_auto : evar_map -> secvars:Id.Pred.t ->
-	       (global_reference * constr array) -> constr -> t -> full_hint list
+               (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val add_one : env -> evar_map -> hint_entry -> t -> t
 val add_list : env -> evar_map -> hint_entry list -> t -> t
-val remove_one : global_reference -> t -> t
-val remove_list : global_reference list -> t -> t
-val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val remove_one : GlobRef.t -> t -> t
+val remove_list : GlobRef.t list -> t -> t
+val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
 val use_dn : t -> bool
 val transparent_state : t -> transparent_state
 val set_transparent_state : t -> transparent_state -> t
 val add_cut : hints_path -> t -> t
-val add_mode : global_reference -> hint_mode array -> t -> t
+val add_mode : GlobRef.t -> hint_mode array -> t -> t
 val cut : t -> hints_path
 val unfolds : t -> Id.Set.t * Cset.t
-val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
   t -> 'a -> 'a
 
 end =
@@ -510,7 +510,7 @@ struct
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
        or with no associated pattern. *)
-    hintdb_nopat : (global_reference option * stored_data) list;
+    hintdb_nopat : (GlobRef.t option * stored_data) list;
     hintdb_name : string option;
   }
 
@@ -664,7 +664,7 @@ struct
 
   let remove_list grs db =
     let filter (_, h) =
-      match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in
+      match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
@@ -1015,9 +1015,9 @@ type hint_action =
   | CreateDB of bool * transparent_state
   | AddTransparency of evaluable_global_reference list * bool
   | AddHints of hint_entry list
-  | RemoveHints of global_reference list
+  | RemoveHints of GlobRef.t list
   | AddCut of hints_path
-  | AddMode of global_reference * hint_mode array
+  | AddMode of GlobRef.t * hint_mode array
 
 let add_cut dbname path =
   let db = get_db dbname in
@@ -1226,7 +1226,7 @@ type hints_entry =
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
-  | HintsModeEntry of global_reference * hint_mode list
+  | HintsModeEntry of GlobRef.t * hint_mode list
   | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
 let default_prepare_hint_ident = Id.of_string "H"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index b06ede0e1..c7de10a2a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
 open Names
 open EConstr
 open Environ
-open Globnames
 open Decl_kinds
 open Evd
 open Misctypes
@@ -25,7 +24,7 @@ open Vernacexpr
 
 exception Bound
 
-val decompose_app_bound : evar_map -> constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array
 
 type debug = Debug | Info | Off
 
@@ -51,7 +50,7 @@ type 'a hints_path_atom_gen =
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
 type 'a with_metadata = private {
@@ -81,7 +80,7 @@ type 'a hints_path_gen =
   | PathEpsilon
 
 type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
     
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
@@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
 val pp_hints_path : hints_path -> Pp.t
 val pp_hint_mode : hint_mode -> Pp.t
 val glob_hints_path_atom :
-  Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+  Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
 val glob_hints_path :
-  Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+  Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
 
 module Hint_db :
   sig
     type t
     val empty : ?name:hint_db_name -> transparent_state -> bool -> t
-    val find : global_reference -> t -> search_entry
+    val find : GlobRef.t -> t -> search_entry
 
     (** All hints which have no pattern.
      * [secvars] represent the set of section variables that
@@ -107,27 +106,27 @@ module Hint_db :
     val map_none : secvars:Id.Pred.t -> t -> full_hint list
 
     (** All hints associated to the reference *)
-    val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+    val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
     val map_existential : evar_map -> secvars:Id.Pred.t ->
-      (global_reference * constr array) -> constr -> t -> full_hint list
+      (GlobRef.t * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments and using the discrimination net. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments. *)
     val map_auto : evar_map -> secvars:Id.Pred.t ->
-       (global_reference * constr array) -> constr -> t -> full_hint list
+       (GlobRef.t * constr array) -> constr -> t -> full_hint list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
-    val remove_one : global_reference -> t -> t
-    val remove_list : global_reference list -> t -> t
-    val iter : (global_reference option ->
+    val remove_one : GlobRef.t -> t -> t
+    val remove_list : GlobRef.t list -> t -> t
+    val iter : (GlobRef.t option ->
                 hint_mode array list -> full_hint list -> unit) -> t -> unit
 
     val use_dn : t -> bool
@@ -147,7 +146,7 @@ type hnf = bool
 type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
 
 type hint_term =
-  | IsGlobRef of global_reference
+  | IsGlobRef of GlobRef.t
   | IsConstr of constr * Univ.ContextSet.t
 
 type hints_entry =
@@ -157,7 +156,7 @@ type hints_entry =
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
-  | HintsModeEntry of global_reference * hint_mode list
+  | HintsModeEntry of GlobRef.t * hint_mode list
   | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
 val searchtable_map : hint_db_name -> hint_db
@@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
 
 val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
-val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
 
 val current_db_names : unit -> String.Set.t
 
@@ -264,7 +263,7 @@ val rewrite_db : hint_db_name
 
 val pr_searchtable : env -> evar_map -> Pp.t
 val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
 val pr_hint_db : Hint_db.t -> Pp.t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b012a7ecd..b8f1ed720 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -294,13 +294,13 @@ let match_with_equation env sigma t =
   let (hdapp,args) = destApp sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind,u) ->
-      if eq_gr (IndRef ind) glob_eq then
+      if GlobRef.equal (IndRef ind) glob_eq then
 	Some (build_coq_eq_data()),hdapp,
 	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if eq_gr (IndRef ind) glob_identity then
+      else if GlobRef.equal (IndRef ind) glob_identity then
 	Some (build_coq_identity_data()),hdapp,
 	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if eq_gr (IndRef ind) glob_jmeq then
+      else if GlobRef.equal (IndRef ind) glob_jmeq then
 	Some (build_coq_jmeq_data()),hdapp,
 	HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
       else
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0697d0f19..f04cda123 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
 
 (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
    [t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr
 
 (** Match a negation *)
 val is_matching_not : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index bc2f60186..cbaf691f1 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -135,7 +135,7 @@ val elimination_sort_of_hyp  : Id.t -> goal sigma -> Sorts.family
 val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
 
 val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
 
 (** Tacticals defined directly in term of Proofview *)
 
@@ -268,5 +268,5 @@ module New : sig
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
+  val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59c035e83..ee76ad077 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3453,7 +3453,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
 type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
-  indref: global_reference option;
+  indref: GlobRef.t option;
   params: rel_context;      (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;               (* number of parameters *)
   predicates: rel_context;  (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7809dbf48..46f782eaa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -16,7 +16,6 @@ open Proof_type
 open Evd
 open Clenv
 open Redexpr
-open Globnames
 open Pattern
 open Unification
 open Misctypes
@@ -177,7 +176,7 @@ val change            :
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> unit Proofview.tactic
 val reduce            : red_expr -> clause -> unit Proofview.tactic
-val unfold_constr     : global_reference -> unit Proofview.tactic
+val unfold_constr     : GlobRef.t -> unit Proofview.tactic
 
 (** {6 Modification of the local context. } *)
 
@@ -253,7 +252,7 @@ val apply_delayed_in :
 type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
-  indref: global_reference option;
+  indref: GlobRef.t option;
   params: rel_context;      (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;               (** number of parameters *)
   predicates: rel_context;  (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 753c608ad..611799990 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -37,7 +37,7 @@ struct
   type 't t =
     | DRel
     | DSort
-    | DRef    of global_reference
+    | DRef    of GlobRef.t
     | DCtx    of 't * 't (* (binding list, subterm) = Prods and LetIns *)
     | DLambda of 't * 't
     | DApp    of 't * 't (* binary app *)