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

21 files changed, 79 insertions, 84 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 84295959f..9d4badc60 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -26,7 +26,7 @@ let name_table =
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * Name.t list
+  | ReqGlobal of GlobRef.t * Name.t list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 65e3c3be5..6a776dc96 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -9,14 +9,13 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Environ
 open Constr
 
-val rename_arguments : bool -> global_reference -> Name.t list -> unit
+val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit
 
 (** [Not_found] is raised if no names are defined for [r] *)
-val arguments_names : global_reference -> Name.t list
+val arguments_names : GlobRef.t -> Name.t list
 
 val rename_type_of_constant : env -> pconstant -> types
 val rename_type_of_inductive : env -> pinductive -> types
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a0804b72b..afa8a12fc 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -37,7 +37,7 @@ type cl_info_typ = {
   cl_param : int
 }
 
-type coe_typ = global_reference
+type coe_typ = GlobRef.t
 
 module CoeTypMap = Refmap_env
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index f8600bbe0..35691ea37 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -36,7 +36,7 @@ type cl_info_typ = {
   cl_param : int }
 
 (** This is the type of coercion kinds *)
-type coe_typ = Globnames.global_reference
+type coe_typ = GlobRef.t
 
 (** This is the type of infos for declared coercions *)
 type coe_info_typ
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e89bbf7c3..3ae04cd4f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -113,7 +113,7 @@ let instance_eq f (x1,c1) (x2,c2) =
   Id.equal x1 x2 && f c1 c2
 
 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
-  | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
+  | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
     Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 84be15552..3c3f75a68 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -17,7 +17,6 @@
    arguments and pattern-matching compilation are not. *)
 
 open Names
-open Globnames
 open Decl_kinds
 open Misctypes
 
@@ -36,7 +35,7 @@ type cases_pattern = [ `any ] cases_pattern_g
 
 (** Representation of an internalized (or in other words globalized) term. *)
 type 'a glob_constr_r =
-  | GRef of global_reference * glob_level list option
+  | GRef of GlobRef.t * glob_level list option
       (** An identifier that represents a reference to an object defined
           either in the (global) environment or in the (local) context. *)
   | GVar of Id.t
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 119ff5222..d87a19d28 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -61,7 +61,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr ->
 
 (** Recursor names utilities *)
 
-val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference
+val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t
 val elimination_suffix : Sorts.family -> string
 val make_elimination_ident : Id.t -> Sorts.family -> Id.t
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 76367b612..7dd0954bc 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Misctypes
 
 (** {5 Patterns} *)
@@ -21,7 +20,7 @@ type case_info_pattern =
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
-  | PRef of global_reference
+  | PRef of GlobRef.t
   | PVar of Id.t
   | PEvar of existential_key * constr_pattern array
   | PRel of int
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 27e457e3b..ccfb7f990 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -30,7 +30,7 @@ let case_info_pattern_eq i1 i2 =
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
-| PRef r1, PRef r2 -> eq_gr r1 r2
+| PRef r1, PRef r2 -> GlobRef.equal r1 r2
 | PVar v1, PVar v2 -> Id.equal v1 v2
 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
   Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 9f0878578..dfbfb147f 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -8,12 +8,12 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open EConstr
-open Globnames
-open Glob_term
+open Names
 open Mod_subst
 open Misctypes
+open Glob_term
 open Pattern
+open EConstr
 open Ltac_pretype
 
 (** {5 Functions on patterns} *)
@@ -32,12 +32,12 @@ exception BoundPattern
    type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
    if [t] is an abstraction *)
 
-val head_pattern_bound : constr_pattern -> global_reference
+val head_pattern_bound : constr_pattern -> GlobRef.t
 
 (** [head_of_constr_reference c] assumes [r] denotes a reference and
    returns its label; raises an anomaly otherwise *)
 
-val head_of_constr_reference : Evd.evar_map -> constr -> global_reference
+val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t
 
 (** [pattern_of_constr c] translates a term [c] with metavariables into
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
diff --git a/pretyping/program.mli b/pretyping/program.mli
index df0848ba1..a8f511578 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -8,37 +8,37 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open EConstr
-open Globnames
 
 (** A bunch of Coq constants used by Progam *)
 
-val sig_typ : unit -> global_reference
-val sig_intro : unit -> global_reference
-val sig_proj1 : unit -> global_reference
-val sigT_typ : unit -> global_reference
-val sigT_intro : unit -> global_reference
-val sigT_proj1 : unit -> global_reference
-val sigT_proj2 : unit -> global_reference
+val sig_typ : unit -> GlobRef.t
+val sig_intro : unit -> GlobRef.t
+val sig_proj1 : unit -> GlobRef.t
+val sigT_typ : unit -> GlobRef.t
+val sigT_intro : unit -> GlobRef.t
+val sigT_proj1 : unit -> GlobRef.t
+val sigT_proj2 : unit -> GlobRef.t
 
-val prod_typ : unit -> global_reference
-val prod_intro : unit -> global_reference
-val prod_proj1 : unit -> global_reference
-val prod_proj2 : unit -> global_reference
+val prod_typ : unit -> GlobRef.t
+val prod_intro : unit -> GlobRef.t
+val prod_proj1 : unit -> GlobRef.t
+val prod_proj2 : unit -> GlobRef.t
 
-val coq_eq_ind : unit -> global_reference
-val coq_eq_refl : unit -> global_reference
-val coq_eq_refl_ref : unit -> global_reference
-val coq_eq_rect : unit -> global_reference
+val coq_eq_ind : unit -> GlobRef.t
+val coq_eq_refl : unit -> GlobRef.t
+val coq_eq_refl_ref : unit -> GlobRef.t
+val coq_eq_rect : unit -> GlobRef.t
 
-val coq_JMeq_ind : unit -> global_reference
-val coq_JMeq_refl : unit -> global_reference
+val coq_JMeq_ind : unit -> GlobRef.t
+val coq_JMeq_refl : unit -> GlobRef.t
 
 val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
 val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
 
 (** Polymorphic application of delayed references *)
-val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
+val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr
 
 val get_proofs_transparency : unit -> bool
 val is_program_cases : unit -> bool
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d070edead..84aceeedd 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -144,13 +144,13 @@ type obj_typ = {
   o_TCOMPS : constr list } (* ordered *)
 
 type cs_pattern =
-    Const_cs of global_reference
+    Const_cs of GlobRef.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
 
 let eq_cs_pattern p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2
+| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2
 | Prod_cs, Prod_cs -> true
 | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
 | Default_cs, Default_cs -> true
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 1f7b23c0c..748f053b2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Globnames
 
 (** Operations concerning records and canonical structures *)
 
@@ -40,10 +39,10 @@ val lookup_structure : inductive -> struc_typ
 val lookup_projections : inductive -> Constant.t option list
 
 (** raise [Not_found] if not a projection *)
-val find_projection_nparams : global_reference -> int
+val find_projection_nparams : GlobRef.t -> int
 
 (** raise [Not_found] if not a projection *)
-val find_projection : global_reference -> struc_typ
+val find_projection : GlobRef.t -> struc_typ
 
 (** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
@@ -52,7 +51,7 @@ val find_projection : global_reference -> struc_typ
 
 (** A cs_pattern characterizes the form of a component of canonical structure *)
 type cs_pattern =
-    Const_cs of global_reference
+    Const_cs of GlobRef.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
@@ -71,9 +70,9 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 
 val pr_cs_pattern : cs_pattern -> Pp.t
 
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
-val declare_canonical_structure : global_reference -> unit
+val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
+val declare_canonical_structure : GlobRef.t -> unit
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
-  ((global_reference * cs_pattern) * obj_typ) list
+  ((GlobRef.t * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 244b8e60b..a4d447902 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -104,7 +104,7 @@ module ReductionBehaviour = struct
   type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
   type req =
     | ReqLocal
-    | ReqGlobal of global_reference * (int list * int * flag list)
+    | ReqGlobal of GlobRef.t * (int list * int * flag list)
 
   let load _ (_,(_,(r, b))) =
     table := Refmap.add r b !table
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b8ac085a7..ad280d9f3 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -25,10 +25,10 @@ module ReductionBehaviour : sig
 
 (** [set is_local ref (recargs, nargs, flags)] *)
   val set :
-    bool -> Globnames.global_reference -> (int list * int * flag list) -> unit
+    bool -> GlobRef.t -> (int list * int * flag list) -> unit
   val get :
-    Globnames.global_reference -> (int list * int * flag list) option
-  val print : Globnames.global_reference -> Pp.t
+    GlobRef.t -> (int list * int * flag list) option
+  val print : GlobRef.t -> Pp.t
 end
 
 (** {6 Support for reduction effects } *)
@@ -41,7 +41,7 @@ val declare_reduction_effect : effect_name ->
   (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
 
 (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *)
-val set_reduction_effect : Globnames.global_reference -> effect_name -> unit
+val set_reduction_effect : GlobRef.t -> effect_name -> unit
 
 (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *)
 val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 696001ab7..5a47acd22 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1279,7 +1279,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
             error_cannot_recognize ref
       | _ ->
 	  try
-	    if eq_gr (fst (global_of_constr sigma c)) ref
+            if GlobRef.equal (fst (global_of_constr sigma c)) ref
 	    then it_mkProd_or_LetIn t l
 	    else raise Not_found
 	  with Not_found ->
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index aa7604f53..e6065dda8 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -14,7 +14,6 @@ open Evd
 open EConstr
 open Reductionops
 open Pattern
-open Globnames
 open Locus
 open Univ
 open Ltac_pretype
@@ -30,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error
 
 val is_evaluable : Environ.env -> evaluable_global_reference -> bool
 
-val error_not_evaluable : Globnames.global_reference -> 'a
+val error_not_evaluable : GlobRef.t -> 'a
 
 val evaluable_of_global_reference :
-  Environ.env -> Globnames.global_reference -> evaluable_global_reference
+  Environ.env -> GlobRef.t -> evaluable_global_reference
 
 val global_of_evaluable_reference :
-  evaluable_global_reference -> Globnames.global_reference
+  evaluable_global_reference -> GlobRef.t
 
 exception Redelimination
 
@@ -88,10 +87,10 @@ val reduce_to_quantified_ind : env ->  evar_map -> types -> (inductive * EInstan
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
-  env ->  evar_map -> global_reference -> types -> types
+  env ->  evar_map -> GlobRef.t -> types -> types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> global_reference -> types -> types
+  env ->  evar_map -> GlobRef.t -> types -> types
 
 val find_hnf_rectype : 
   env ->  evar_map -> types -> (inductive * EInstance.t) * constr list
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e73a78fb8..4386144fe 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -71,10 +71,10 @@ type typeclass = {
   cl_univs : Univ.AUContext.t;
 
   (* The class implementation *)
-  cl_impl : global_reference;
+  cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : global_reference option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
@@ -91,12 +91,12 @@ type typeclass = {
 type typeclasses = typeclass Refmap.t
 
 type instance = {
-  is_class: global_reference;
+  is_class: GlobRef.t;
   is_info: hint_info_expr;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
-  is_impl: global_reference;
+  is_impl: GlobRef.t;
 }
 
 type instances = (instance Refmap.t) Refmap.t
@@ -480,7 +480,7 @@ let instances r =
   let cl = class_info r in instances_of cl    
 
 let is_class gr = 
-  Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes
+  Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
 let is_instance = function
   | ConstRef c ->
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e50d90b15..2a8e0b874 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -31,11 +31,11 @@ type typeclass = {
 
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
-  cl_impl : global_reference;
+  cl_impl : GlobRef.t;
 
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
       The global reference gives a direct link to the class itself. *)
-  cl_context : global_reference option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Context.Rel.t;
 
   (** Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
@@ -56,17 +56,17 @@ type typeclass = {
 
 type instance
 
-val instances : global_reference -> instance list
+val instances : GlobRef.t -> instance list
 val typeclasses : unit -> typeclass list
 val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance
+val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
 
-val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
+val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *)
 
 
 (** These raise a UserError if not a class.
@@ -80,12 +80,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
 (** Just return None if not a class *)
 val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
   
-val instance_impl : instance -> global_reference
+val instance_impl : instance -> GlobRef.t
 
 val hint_priority : instance -> int option
 
-val is_class : global_reference -> bool
-val is_instance : global_reference -> bool
+val is_class : GlobRef.t -> bool
+val is_instance : GlobRef.t -> bool
 
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
@@ -127,24 +127,24 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val classes_transparent_state_hook : (unit -> transparent_state) Hook.t
 val classes_transparent_state : unit -> transparent_state
 
-val add_instance_hint_hook : 
-  (global_reference_or_constr -> global_reference list ->
+val add_instance_hint_hook :
+  (global_reference_or_constr -> GlobRef.t list ->
    bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
-val remove_instance_hint_hook : (global_reference -> unit) Hook.t
-val add_instance_hint : global_reference_or_constr -> global_reference list -> 
+val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
+val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
   bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
-val remove_instance_hint : global_reference -> unit
+val remove_instance_hint : GlobRef.t -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : hint_info_expr option -> bool -> global_reference -> unit
+val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)
 
-val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t ->
                        hint_info_expr ->
-                       (global_reference list * hint_info_expr * constr) list
+                       (GlobRef.t list * hint_info_expr * constr) list
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index e10c81c24..89c5d7e7b 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,17 +9,17 @@
 (************************************************************************)
 
 (*i*)
+open Names
 open EConstr
 open Environ
 open Constrexpr
-open Globnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *)
+    | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
     | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index d98295658..4aabc0aee 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,23 +8,23 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open EConstr
 open Environ
 open Constrexpr
-open Globnames
 
 type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
-  | UnboundMethod of global_reference * Misctypes.lident (** Class name, method *)
+  | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
   | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
 val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> global_reference -> Misctypes.lident -> 'a
+val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a