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

11 files changed, 79 insertions, 86 deletions

diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 78545c8bd..07237d750 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Miniml
 
 (** By default, in module Format, you can do horizontal placing of blocks
@@ -54,7 +53,7 @@ val opened_libraries : unit -> ModPath.t list
 
 type kind = Term | Type | Cons | Mod
 
-val pp_global : kind -> global_reference -> string
+val pp_global : kind -> GlobRef.t -> string
 val pp_module : ModPath.t -> string
 
 val top_visible_mp : unit -> ModPath.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 397cb2920..bebd27e11 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -79,7 +79,7 @@ module type VISIT = sig
 
   (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_ref : global_reference -> unit
+  val add_ref : GlobRef.t -> unit
   val add_kn : KerName.t -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 591d3bb86..77f1fb5ef 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -12,7 +12,6 @@
 
 open Names
 open Libnames
-open Globnames
 
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
@@ -26,7 +25,7 @@ val extract_and_compile : reference list -> unit
 (* For debug / external output via coqtop.byte + Drop : *)
 
 val mono_environment :
- global_reference list -> ModPath.t list -> Miniml.ml_structure
+ GlobRef.t list -> ModPath.t list -> Miniml.ml_structure
 
 (* Used by the Relation Extraction plugin *)
 
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index e1e49d926..ce920ad6a 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -11,7 +11,6 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Names
-open Globnames
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
@@ -26,7 +25,7 @@ open Globnames
 type kill_reason =
   | Ktype
   | Kprop
-  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
+  | Kimplicit of GlobRef.t * int  (* n-th arg of a cst or construct *)
 
 type sign = Keep | Kill of kill_reason
 
@@ -39,7 +38,7 @@ type signature = sign list
 
 type ml_type =
   | Tarr    of ml_type * ml_type
-  | Tglob   of global_reference * ml_type list
+  | Tglob   of GlobRef.t * ml_type list
   | Tvar    of int
   | Tvar'   of int (* same as Tvar, used to avoid clash *)
   | Tmeta   of ml_meta (* used during ML type reconstruction *)
@@ -60,7 +59,7 @@ type inductive_kind =
   | Singleton
   | Coinductive
   | Standard
-  | Record of global_reference option list (* None for anonymous field *)
+  | Record of GlobRef.t option list (* None for anonymous field *)
 
 (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
    If the inductive is logical ([ip_logical = false]), then all other fields
@@ -118,8 +117,8 @@ and ml_ast =
   | MLapp    of ml_ast * ml_ast list
   | MLlam    of ml_ident * ml_ast
   | MLletin  of ml_ident * ml_ast * ml_ast
-  | MLglob   of global_reference
-  | MLcons   of ml_type * global_reference * ml_ast list
+  | MLglob   of GlobRef.t
+  | MLcons   of ml_type * GlobRef.t * ml_ast list
   | MLtuple  of ml_ast list
   | MLcase   of ml_type * ml_ast * ml_branch array
   | MLfix    of int * Id.t array * ml_ast array
@@ -129,24 +128,24 @@ and ml_ast =
   | MLmagic  of ml_ast
 
 and ml_pattern =
-  | Pcons   of global_reference * ml_pattern list
+  | Pcons   of GlobRef.t * ml_pattern list
   | Ptuple  of ml_pattern list
   | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
   | Pwild
-  | Pusual  of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+  | Pusual  of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
 
 (*s ML declarations. *)
 
 type ml_decl =
   | Dind  of MutInd.t * ml_ind
-  | Dtype of global_reference * Id.t list * ml_type
-  | Dterm of global_reference * ml_ast * ml_type
-  | Dfix  of global_reference array * ml_ast array * ml_type array
+  | Dtype of GlobRef.t * Id.t list * ml_type
+  | Dterm of GlobRef.t * ml_ast * ml_type
+  | Dfix  of GlobRef.t array * ml_ast array * ml_type array
 
 type ml_spec =
   | Sind  of MutInd.t * ml_ind
-  | Stype of global_reference * Id.t list * ml_type option
-  | Sval  of global_reference * ml_type
+  | Stype of GlobRef.t * Id.t list * ml_type option
+  | Sval  of GlobRef.t * ml_type
 
 type ml_specif =
   | Spec of ml_spec
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index e1e49d926..ce920ad6a 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -11,7 +11,6 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Names
-open Globnames
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
@@ -26,7 +25,7 @@ open Globnames
 type kill_reason =
   | Ktype
   | Kprop
-  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
+  | Kimplicit of GlobRef.t * int  (* n-th arg of a cst or construct *)
 
 type sign = Keep | Kill of kill_reason
 
@@ -39,7 +38,7 @@ type signature = sign list
 
 type ml_type =
   | Tarr    of ml_type * ml_type
-  | Tglob   of global_reference * ml_type list
+  | Tglob   of GlobRef.t * ml_type list
   | Tvar    of int
   | Tvar'   of int (* same as Tvar, used to avoid clash *)
   | Tmeta   of ml_meta (* used during ML type reconstruction *)
@@ -60,7 +59,7 @@ type inductive_kind =
   | Singleton
   | Coinductive
   | Standard
-  | Record of global_reference option list (* None for anonymous field *)
+  | Record of GlobRef.t option list (* None for anonymous field *)
 
 (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
    If the inductive is logical ([ip_logical = false]), then all other fields
@@ -118,8 +117,8 @@ and ml_ast =
   | MLapp    of ml_ast * ml_ast list
   | MLlam    of ml_ident * ml_ast
   | MLletin  of ml_ident * ml_ast * ml_ast
-  | MLglob   of global_reference
-  | MLcons   of ml_type * global_reference * ml_ast list
+  | MLglob   of GlobRef.t
+  | MLcons   of ml_type * GlobRef.t * ml_ast list
   | MLtuple  of ml_ast list
   | MLcase   of ml_type * ml_ast * ml_branch array
   | MLfix    of int * Id.t array * ml_ast array
@@ -129,24 +128,24 @@ and ml_ast =
   | MLmagic  of ml_ast
 
 and ml_pattern =
-  | Pcons   of global_reference * ml_pattern list
+  | Pcons   of GlobRef.t * ml_pattern list
   | Ptuple  of ml_pattern list
   | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
   | Pwild
-  | Pusual  of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+  | Pusual  of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
 
 (*s ML declarations. *)
 
 type ml_decl =
   | Dind  of MutInd.t * ml_ind
-  | Dtype of global_reference * Id.t list * ml_type
-  | Dterm of global_reference * ml_ast * ml_type
-  | Dfix  of global_reference array * ml_ast array * ml_type array
+  | Dtype of GlobRef.t * Id.t list * ml_type
+  | Dterm of GlobRef.t * ml_ast * ml_type
+  | Dfix  of GlobRef.t array * ml_ast array * ml_type array
 
 type ml_spec =
   | Sind  of MutInd.t * ml_ind
-  | Stype of global_reference * Id.t list * ml_type option
-  | Sval  of global_reference * ml_type
+  | Stype of GlobRef.t * Id.t list * ml_type option
+  | Sval  of GlobRef.t * ml_type
 
 type ml_specif =
   | Spec of ml_spec
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 0656d487a..0901acc7d 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -59,7 +59,7 @@ let rec eq_ml_type t1 t2 = match t1, t2 with
 | Tarr (tl1, tr1), Tarr (tl2, tr2) ->
   eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
 | Tglob (gr1, t1), Tglob (gr2, t2) ->
-  eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+  GlobRef.equal gr1 gr2 && List.equal eq_ml_type t1 t2
 | Tvar i1, Tvar i2 -> Int.equal i1 i2
 | Tvar' i1, Tvar' i2 -> Int.equal i1 i2
 | Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
@@ -120,7 +120,7 @@ let rec mgu = function
       | None -> m.contents <- Some t)
   | Tarr(a, b), Tarr(a', b') ->
       mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
+  | Tglob (r,l), Tglob (r',l') when GlobRef.equal r r' ->
        List.iter mgu (List.combine l l')
   | Tdummy _, Tdummy _ -> ()
   | Tvar i, Tvar j when Int.equal i j -> ()
@@ -270,7 +270,7 @@ let rec var2var' = function
   | Tglob (r,l) -> Tglob (r, List.map var2var' l)
   | a -> a
 
-type abbrev_map = global_reference -> ml_type option
+type abbrev_map = GlobRef.t -> ml_type option
 
 (*s Delta-reduction of type constants everywhere in a ML type [t].
    [env] is a function of type [ml_type_env]. *)
@@ -381,9 +381,9 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
   eq_ml_ident na1 na2 && eq_ml_ast t1 t2
 | MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
   eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
-| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLglob gr1, MLglob gr2 -> GlobRef.equal gr1 gr2
 | MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
-  eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+  eq_ml_type t1 t2 && GlobRef.equal gr1 gr2 && List.equal eq_ml_ast c1 c2
 | MLtuple t1, MLtuple t2 ->
   List.equal eq_ml_ast t1 t2
 | MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
@@ -398,13 +398,13 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 
 and eq_ml_pattern p1 p2 = match p1, p2 with
 | Pcons (gr1, p1), Pcons (gr2, p2) ->
-  eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+  GlobRef.equal gr1 gr2 && List.equal eq_ml_pattern p1 p2
 | Ptuple p1, Ptuple p2 ->
   List.equal eq_ml_pattern p1 p2
 | Prel i1, Prel i2 ->
   Int.equal i1 i2
 | Pwild, Pwild -> true
-| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| Pusual gr1, Pusual gr2 -> GlobRef.equal gr1 gr2
 | _ -> false
 
 and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
@@ -984,7 +984,7 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
   if i >= Array.length br then raise Impossible;
   let (ids,p,c) = br.(i) in
   match p with
-    | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
+    | Pusual r' | Pcons (r',_) when not (GlobRef.equal r' r) -> iota_red (i+1) lift br cons
     | Pusual r' ->
       let c = named_lams (List.rev ids) c in
       let c = ast_lift lift c
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 55a1ee893..d23fdb3d5 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Miniml
 open Table
 
@@ -59,7 +58,7 @@ val type_recomp : ml_type list * ml_type -> ml_type
 
 val var2var' : ml_type -> ml_type
 
-type abbrev_map = global_reference -> ml_type option
+type abbrev_map = GlobRef.t -> ml_type option
 
 val type_expand : abbrev_map -> ml_type -> ml_type
 val type_simpl : ml_type -> ml_type
@@ -117,7 +116,7 @@ val dump_unused_vars : ml_ast -> ml_ast
 
 val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
-val inline : global_reference -> ml_ast -> bool
+val inline : GlobRef.t -> ml_ast -> bool
 
 val is_basic_pattern : ml_pattern -> bool
 val has_deep_pattern : ml_branch array -> bool
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index f33a59edf..b398bc07a 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -76,7 +76,7 @@ let struct_iter do_decl do_spec do_mp s =
 (*s Apply some fonctions upon all references in [ml_type], [ml_ast],
   [ml_decl], [ml_spec] and [ml_structure]. *)
 
-type do_ref = global_reference -> unit
+type do_ref = GlobRef.t -> unit
 
 let record_iter_references do_term = function
   | Record l -> List.iter (Option.iter do_term) l
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 6a81f2705..f45773f09 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Miniml
 
 (*s Functions upon ML modules. *)
@@ -17,7 +16,7 @@ open Miniml
 val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
 val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
-type do_ref = global_reference -> unit
+type do_ref = GlobRef.t -> unit
 
 val type_iter_references : do_ref -> ml_type -> unit
 val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
@@ -30,7 +29,7 @@ val mtyp_of_mexpr : ml_module_expr -> ml_module_type
 
 val msid_of_mt : ml_module_type -> ModPath.t
 
-val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
+val get_decl_in_structure : GlobRef.t -> ml_structure -> ml_decl
 
 (* Some transformations of ML terms. [optimize_struct] simplify
    all beta redexes (when the argument does not occur, it is just
@@ -39,5 +38,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    optimizations. The first argument is the list of objects we want to appear.
 *)
 
-val optimize_struct : global_reference list * ModPath.t list ->
+val optimize_struct : GlobRef.t list * ModPath.t list ->
   ml_structure -> ml_structure
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 54c6d9d72..c3f4cfe65 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -652,7 +652,7 @@ let add_inline_entries b l =
 
 (* Registration of operations for rollback. *)
 
-let inline_extraction : bool * global_reference list -> obj =
+let inline_extraction : bool * GlobRef.t list -> obj =
   declare_object
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
@@ -736,7 +736,7 @@ let add_implicits r l =
 
 (* Registration of operations for rollback. *)
 
-let implicit_extraction : global_reference * int_or_id list -> obj =
+let implicit_extraction : GlobRef.t * int_or_id list -> obj =
   declare_object
     {(default_object "Extraction Implicit") with
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
@@ -857,7 +857,7 @@ let find_custom_match pv =
 
 (* Registration of operations for rollback. *)
 
-let in_customs : global_reference * string list * string -> obj =
+let in_customs : GlobRef.t * string list * string -> obj =
   declare_object
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -867,7 +867,7 @@ let in_customs : global_reference * string list * string -> obj =
         (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
 
-let in_custom_matchs : global_reference * string -> obj =
+let in_custom_matchs : GlobRef.t * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 906dfd96e..5bf944434 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -10,31 +10,30 @@
 
 open Names
 open Libnames
-open Globnames
 open Miniml
 open Declarations
 
-module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : CSig.MapS with type key = global_reference
+module Refset' : CSig.SetS with type elt = GlobRef.t
+module Refmap' : CSig.MapS with type key = GlobRef.t
 
-val safe_basename_of_global : global_reference -> Id.t
+val safe_basename_of_global : GlobRef.t -> Id.t
 
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * GlobRef.t -> unit
 val warning_id : string -> unit
-val error_axiom_scheme : global_reference -> int -> 'a
-val error_constant : global_reference -> 'a
-val error_inductive : global_reference -> 'a
+val error_axiom_scheme : GlobRef.t -> int -> 'a
+val error_constant : GlobRef.t -> 'a
+val error_inductive : GlobRef.t -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : ModPath.t -> ModPath.t -> 'a
 val error_no_module_expr : ModPath.t -> 'a
-val error_singleton_become_prop : Id.t -> global_reference option -> 'a
+val error_singleton_become_prop : Id.t -> GlobRef.t option -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
-val error_not_visible : global_reference -> 'a
+val error_not_visible : GlobRef.t -> 'a
 val error_MPfile_as_mod : ModPath.t -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
@@ -44,12 +43,12 @@ val err_or_warn_remaining_implicit : kill_reason -> unit
 
 val info_file : string -> unit
 
-(*s utilities about [module_path] and [kernel_names] and [global_reference] *)
+(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
 
-val occur_kn_in_ref : MutInd.t -> global_reference -> bool
-val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t
-val modpath_of_r : global_reference -> ModPath.t
-val label_of_r : global_reference -> Label.t
+val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
+val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val modpath_of_r : GlobRef.t -> ModPath.t
+val label_of_r : GlobRef.t -> Label.t
 val base_mp : ModPath.t -> ModPath.t
 val is_modfile : ModPath.t -> bool
 val string_of_modfile : ModPath.t -> string
@@ -61,7 +60,7 @@ val prefixes_mp : ModPath.t -> MPset.t
 val common_prefix_from_list :
   ModPath.t -> ModPath.t list -> ModPath.t option
 val get_nth_label_mp : int -> ModPath.t -> Label.t
-val labels_of_ref : global_reference -> ModPath.t * Label.t list
+val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list
 
 (*s Some table-related operations *)
 
@@ -83,27 +82,27 @@ val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
 
 val add_inductive_kind : MutInd.t -> inductive_kind -> unit
-val is_coinductive : global_reference -> bool
+val is_coinductive : GlobRef.t -> bool
 val is_coinductive_type : ml_type -> bool
 (* What are the fields of a record (empty for a non-record) *)
 val get_record_fields :
-  global_reference -> global_reference option list
-val record_fields_of_type : ml_type -> global_reference option list
+  GlobRef.t -> GlobRef.t option list
+val record_fields_of_type : ml_type -> GlobRef.t option list
 
 val add_recursors : Environ.env -> MutInd.t -> unit
-val is_recursor : global_reference -> bool
+val is_recursor : GlobRef.t -> bool
 
 val add_projection : int -> Constant.t -> inductive -> unit
-val is_projection : global_reference -> bool
-val projection_arity : global_reference -> int
-val projection_info : global_reference -> inductive * int (* arity *)
+val is_projection : GlobRef.t -> bool
+val projection_arity : GlobRef.t -> int
+val projection_info : GlobRef.t -> inductive * int (* arity *)
 
-val add_info_axiom : global_reference -> unit
-val remove_info_axiom : global_reference -> unit
-val add_log_axiom : global_reference -> unit
+val add_info_axiom : GlobRef.t -> unit
+val remove_info_axiom : GlobRef.t -> unit
+val add_log_axiom : GlobRef.t -> unit
 
-val add_opaque : global_reference -> unit
-val remove_opaque : global_reference -> unit
+val add_opaque : GlobRef.t -> unit
+val remove_opaque : GlobRef.t -> unit
 
 val reset_tables : unit -> unit
 
@@ -172,22 +171,22 @@ val is_extrcompute : unit -> bool
 
 (*s Table for custom inlining *)
 
-val to_inline : global_reference -> bool
-val to_keep : global_reference -> bool
+val to_inline : GlobRef.t -> bool
+val to_keep : GlobRef.t -> bool
 
 (*s Table for implicits arguments *)
 
-val implicits_of_global : global_reference -> Int.Set.t
+val implicits_of_global : GlobRef.t -> Int.Set.t
 
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
 val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
 
-val is_custom : global_reference -> bool
-val is_inline_custom : global_reference -> bool
-val find_custom : global_reference -> string
-val find_type_custom : global_reference -> string list * string
+val is_custom : GlobRef.t -> bool
+val is_inline_custom : GlobRef.t -> bool
+val find_custom : GlobRef.t -> string
+val find_type_custom : GlobRef.t -> string list * string
 
 val is_custom_match : ml_branch array -> bool
 val find_custom_match : ml_branch array -> string