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

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 8ab70283c..6f5887ca2 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -13,7 +13,6 @@ open Termops
 open EConstr
 open Environ
 open Libnames
-open Globnames
 open Glob_term
 open Pattern
 open Constrexpr
@@ -40,7 +39,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -58,9 +57,9 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
 val get_extern_reference :
-  unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
 
 (** WARNING: The following functions are evil due to
     side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7eda89f4e..def8425ec 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1077,7 +1077,7 @@ let interp_reference vars r =
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
   | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
-  | RCPatCstr  of Globnames.global_reference
+  | RCPatCstr  of GlobRef.t
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
   (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
   | RCPatAtom  of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
@@ -1314,7 +1314,7 @@ let sort_fields ~complete loc fields completer =
               | [] -> (idx, acc_first_idx, acc)
               | (Some field_glob_id) :: projs ->
                  let field_glob_ref = ConstRef field_glob_id in
-                 let first_field = eq_gr field_glob_ref first_field_glob_ref in
+                 let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
                     | (_, regular) :: proj_kinds ->
@@ -1352,7 +1352,7 @@ let sort_fields ~complete loc fields completer =
                  user_err ?loc ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+                 let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    user_err ?loc 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f5e32dc4c..4dd719e1f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -13,7 +13,6 @@ open Evd
 open Environ
 open Misctypes
 open Libnames
-open Globnames
 open Glob_term
 open Pattern
 open EConstr
@@ -143,7 +142,7 @@ val intern_constr_pattern :
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> global_reference
+val intern_reference : reference -> GlobRef.t
 
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> reference -> glob_constr
@@ -175,11 +174,11 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
-val locate_reference :  Libnames.qualid -> Globnames.global_reference
+val locate_reference :  Libnames.qualid -> GlobRef.t
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
-val global_reference : Id.t -> Globnames.global_reference
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
+val global_reference : Id.t -> GlobRef.t
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)
diff --git a/interp/declare.mli b/interp/declare.mli
index 084d746e6..f8cffbb1e 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) ->
 val exists_name : Id.t -> bool
 
 (** Global universe contexts, names and constraints *)
-val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 43c100008..8dfb4f8f7 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -24,7 +24,7 @@ val feedback_glob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
 val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
 val dump_definition : Misctypes.lident -> bool -> string -> unit
@@ -43,4 +43,4 @@ val dump_constraint :
 
 val dump_string : string -> unit
 
-val type_of_global_ref : Globnames.global_reference -> string 
+val type_of_global_ref : Names.GlobRef.t -> string
diff --git a/interp/impargs.ml b/interp/impargs.ml
index b424f73de..7e4c4ef4f 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -505,7 +505,7 @@ type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of Constant.t * implicits_flags
   | ImplMutualInductive of MutInd.t * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags *
+  | ImplInteractive of GlobRef.t * implicits_flags *
       implicit_interactive_request
 
 let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
@@ -626,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with
 
 type implicits_obj =
     implicit_discharge_request *
-      (global_reference * implicits_list list) list
+      (GlobRef.t * implicits_list list) list
 
 let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 103a4f9e9..ea5aa90f6 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Globnames
 open Environ
 
 (** {6 Implicit Arguments } *)
@@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit
 val declare_constant_implicits : Constant.t -> unit
 val declare_mib_implicits : MutInd.t -> unit
 
-val declare_implicits : bool -> global_reference -> unit
+val declare_implicits : bool -> GlobRef.t -> unit
 
 (** [declare_manual_implicits local ref enriching l]
    Manual declaration of which arguments are expected implicit.
@@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit
    implicits depending on the current state.
    Unsets implicits if [l] is empty. *)
 
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits list -> unit
 
 (** If the list is empty, do nothing, otherwise declare the implicits. *)
 
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits -> unit
 
-val implicits_of_global : global_reference -> implicits_list list
+val implicits_of_global : GlobRef.t -> implicits_list list
 
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b9815f34d..5f4129ae0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -12,7 +12,6 @@ open Names
 open Glob_term
 open Constrexpr
 open Libnames
-open Globnames
 
 val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
 
@@ -39,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+  Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+  (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/notation.ml b/interp/notation.ml
index 47d648135..4a6d2a154 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -259,7 +259,7 @@ type interp_rule =
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
 type key =
-  | RefKey of global_reference
+  | RefKey of GlobRef.t
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
@@ -778,7 +778,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
       (req,r,0,l1@l,cls1)
 
 type arguments_scope_obj =
-    arguments_scope_discharge_request * global_reference *
+    arguments_scope_discharge_request * GlobRef.t *
     (* Used to communicate information from discharge to rebuild *)
     (* set to 0 otherwise *) int *
     scope_name option list * scope_class option list
diff --git a/interp/notation.mli b/interp/notation.mli
index 6803a7e51..eac87414f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -11,7 +11,6 @@
 open Bigint
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Glob_term
 open Notation_term
@@ -91,7 +90,7 @@ val declare_string_interpreter : scope_name -> required_module ->
 val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
 (* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
   local_scopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
@@ -143,8 +142,8 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
 (** {6 Miscellaneous} *)
 
-val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
-      notation -> delimiters option -> global_reference
+val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+      notation -> delimiters option -> GlobRef.t
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
@@ -152,9 +151,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
 
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
-  bool (** true=local *) -> global_reference -> scope_name option list -> unit
+  bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
 
-val find_arguments_scope : global_reference -> scope_name option list
+val find_arguments_scope : GlobRef.t -> scope_name option list
 
 type scope_class
 
@@ -165,7 +164,7 @@ val subst_scope_class :
   Mod_subst.substitution -> scope_class -> scope_class option
 
 val declare_scope_class : scope_name -> scope_class -> unit
-val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit
+val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
 
 val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
 val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a76f82094..6a282624e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -28,7 +28,7 @@ open Notation_term
 let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
 
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
 | NVar id1, NVar id2 -> (
    match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
    | Some n,Some m -> Int.equal n m
@@ -1123,7 +1123,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
-  | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+  | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
   | GApp (f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index a9c2e2a53..1a46746cc 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Misctypes
 open Glob_term
 
@@ -23,7 +22,7 @@ open Glob_term
 
 type notation_constr =
   (** Part common to [glob_constr] and [cases_pattern] *)
-  | NRef of global_reference
+  | NRef of GlobRef.t
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 36005121b..b57103cf2 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ open Notation_ops
 open Globnames
 
 type key =
-  | RefKey of global_reference
+  | RefKey of GlobRef.t
   | Oth
 
 (** TODO: share code from Notation *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 7ff7e899e..45037b8b3 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -18,22 +18,22 @@ open Misctypes
    if not bound in the global env; raise a [UserError] if bound to a
    syntactic def that does not denote a reference *)
 
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t
 
 (** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> global_reference
+val global_of_extended_global : extended_global_reference -> GlobRef.t
 
 (** Locate a reference taking into account possible "alias" notations.
     May raise [Nametab.GlobalizationError _] for an unknown reference,
     or a [UserError] if bound to a syntactic def that does not denote
     a reference. *)
-val global_with_alias : ?head:bool -> reference -> global_reference
+val global_with_alias : ?head:bool -> reference -> GlobRef.t
 
 (** The same for inductive types *)
 val global_inductive_with_alias : reference -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> global_reference
+val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
 
 (** The same for inductive types *)
 val smart_global_inductive : reference or_by_notation -> inductive
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 53d1a522d..dc9c370a1 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,7 +14,6 @@ open Loc
 open Names
 open EConstr
 open Libnames
-open Globnames
 open Genredexpr
 open Pattern
 open Constrexpr
@@ -42,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type
 
 val wit_var : (lident, lident, Id.t) genarg_type
 
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
@@ -81,8 +80,8 @@ val wit_clause_dft_concl :  (lident Locus.clause_expr, lident Locus.clause_expr,
 
 val wit_integer : int uniform_genarg_type
 val wit_preident : string uniform_genarg_type
-val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
 val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type