[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, 168 insertions, 174 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 3f01c617c..408e25919 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -171,16 +171,16 @@ let jmeq_kn = make_ind jmeq_module "JMeq"
 let glob_jmeq = IndRef (jmeq_kn,0)
 
 type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
+  proj1 : GlobRef.t;
+  proj2 : GlobRef.t;
+  elim  : GlobRef.t;
+  intro : GlobRef.t;
+  typ   : GlobRef.t }
 
 type coq_bool_data  = {
-  andb : global_reference;
-  andb_prop : global_reference;
-  andb_true_intro : global_reference}
+  andb : GlobRef.t;
+  andb_prop : GlobRef.t;
+  andb_true_intro : GlobRef.t}
 
 let build_bool_type () =
   { andb =  init_reference ["Datatypes"] "andb";
@@ -213,18 +213,18 @@ let build_prod () =
 
 (* Equalities *)
 type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
+  eq   : GlobRef.t;
+  ind  : GlobRef.t;
+  refl : GlobRef.t;
+  sym  : GlobRef.t;
+  trans: GlobRef.t;
+  congr: GlobRef.t }
 
 (* Data needed for discriminate and injection *)
 type coq_inversion_data = {
-  inv_eq   : global_reference; (* : forall params, t -> Prop *)
-  inv_ind  : global_reference; (* : forall params P y, eq params y -> P y *)
-  inv_congr: global_reference  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+  inv_eq   : GlobRef.t; (* : forall params, t -> Prop *)
+  inv_ind  : GlobRef.t; (* : forall params P y, eq params y -> P y *)
+  inv_congr: GlobRef.t  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
 }
 
 let lazy_init_reference dir id = lazy (init_reference dir id)
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 8077c47c7..b4bd1b0e0 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -8,10 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Names
 open Libnames
-open Globnames
-open Util
 
 (** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
@@ -44,14 +43,14 @@ open Util
 
 type message = string
 
-val find_reference : message -> string list -> string -> global_reference
-val coq_reference : message -> string list -> string -> global_reference
+val find_reference : message -> string list -> string -> GlobRef.t
+val coq_reference : message -> string list -> string -> GlobRef.t
 
 (** For tactics/commands requiring vernacular libraries *)
 val check_required_library : string list -> unit
 
 (** Search in several modules (not prefixed by "Coq") *)
-val gen_reference_in_modules : string->string list list-> string -> global_reference
+val gen_reference_in_modules : string->string list list-> string -> GlobRef.t
 
 val arith_modules : string list list
 val zarith_base_modules : string list list
@@ -78,24 +77,24 @@ val type_of_id : Constant.t
 
 (** Natural numbers *)
 val nat_path : full_path
-val glob_nat : global_reference
+val glob_nat : GlobRef.t
 val path_of_O : constructor
 val path_of_S : constructor
-val glob_O : global_reference
-val glob_S : global_reference
+val glob_O : GlobRef.t
+val glob_S : GlobRef.t
 
 (** Booleans *)
-val glob_bool : global_reference
+val glob_bool : GlobRef.t
 val path_of_true : constructor
 val path_of_false : constructor
-val glob_true : global_reference
-val glob_false : global_reference
+val glob_true : GlobRef.t
+val glob_false : GlobRef.t
 
 
 (** Equality *)
-val glob_eq : global_reference
-val glob_identity : global_reference
-val glob_jmeq : global_reference
+val glob_eq : GlobRef.t
+val glob_identity : GlobRef.t
+val glob_jmeq : GlobRef.t
 
 (** {6 ... } *)
 (** Constructions and patterns related to Coq initial state are unknown
@@ -106,18 +105,18 @@ val glob_jmeq : global_reference
    at runtime. *)
 
 type coq_bool_data = {
-  andb : global_reference;
-  andb_prop : global_reference;
-  andb_true_intro : global_reference}
+  andb : GlobRef.t;
+  andb_prop : GlobRef.t;
+  andb_true_intro : GlobRef.t}
 val build_bool_type : coq_bool_data delayed
 
 (** {6 For Equality tactics } *)
 type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
+  proj1 : GlobRef.t;
+  proj2 : GlobRef.t;
+  elim  : GlobRef.t;
+  intro : GlobRef.t;
+  typ   : GlobRef.t }
 
 val build_sigma_set : coq_sigma_data delayed
 val build_sigma_type : coq_sigma_data delayed
@@ -132,30 +131,30 @@ val build_sigma : coq_sigma_data delayed
 val build_prod : coq_sigma_data delayed
 
 type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
+  eq   : GlobRef.t;
+  ind  : GlobRef.t;
+  refl : GlobRef.t;
+  sym  : GlobRef.t;
+  trans: GlobRef.t;
+  congr: GlobRef.t }
 
 val build_coq_eq_data : coq_eq_data delayed
 
 val build_coq_identity_data : coq_eq_data delayed
 val build_coq_jmeq_data : coq_eq_data delayed
 
-val build_coq_eq       : global_reference delayed (** = [(build_coq_eq_data()).eq] *)
-val build_coq_eq_refl  : global_reference delayed (** = [(build_coq_eq_data()).refl] *)
-val build_coq_eq_sym   : global_reference delayed (** = [(build_coq_eq_data()).sym] *)
-val build_coq_f_equal2 : global_reference delayed
+val build_coq_eq       : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl  : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym   : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *)
+val build_coq_f_equal2 : GlobRef.t delayed
 
 (** Data needed for discriminate and injection *)
 
 type coq_inversion_data = {
-  inv_eq   : global_reference; (** : forall params, args -> Prop *)
-  inv_ind  : global_reference; (** : forall params P (H : P params) args, eq params args 
+  inv_eq   : GlobRef.t; (** : forall params, args -> Prop *)
+  inv_ind  : GlobRef.t; (** : forall params P (H : P params) args, eq params args
 			 ->  P args *)
-  inv_congr: global_reference  (** : forall params B (f:t->B) args, eq params args -> 
+  inv_congr: GlobRef.t  (** : forall params B (f:t->B) args, eq params args ->
 			 f params = f args *)
 }
 
@@ -165,45 +164,45 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed
 val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
 (** Specif *)
-val build_coq_sumbool : global_reference delayed
+val build_coq_sumbool : GlobRef.t delayed
 
 (** {6 ... } *)
 (** Connectives 
    The False proposition *)
-val build_coq_False : global_reference delayed
+val build_coq_False : GlobRef.t delayed
 
 (** The True proposition and its unique proof *)
-val build_coq_True : global_reference delayed
-val build_coq_I : global_reference delayed
+val build_coq_True : GlobRef.t delayed
+val build_coq_I : GlobRef.t delayed
 
 (** Negation *)
-val build_coq_not : global_reference delayed
+val build_coq_not : GlobRef.t delayed
 
 (** Conjunction *)
-val build_coq_and : global_reference delayed
-val build_coq_conj : global_reference delayed
-val build_coq_iff : global_reference delayed
+val build_coq_and : GlobRef.t delayed
+val build_coq_conj : GlobRef.t delayed
+val build_coq_iff : GlobRef.t delayed
 
-val build_coq_iff_left_proj : global_reference delayed
-val build_coq_iff_right_proj : global_reference delayed
+val build_coq_iff_left_proj : GlobRef.t delayed
+val build_coq_iff_right_proj : GlobRef.t delayed
 
 (** Disjunction *)
-val build_coq_or : global_reference delayed
+val build_coq_or : GlobRef.t delayed
 
 (** Existential quantifier *)
-val build_coq_ex : global_reference delayed
-
-val coq_eq_ref : global_reference lazy_t
-val coq_identity_ref : global_reference lazy_t
-val coq_jmeq_ref : global_reference lazy_t
-val coq_eq_true_ref : global_reference lazy_t
-val coq_existS_ref : global_reference lazy_t
-val coq_existT_ref : global_reference lazy_t
-val coq_exist_ref : global_reference lazy_t
-val coq_not_ref : global_reference lazy_t
-val coq_False_ref : global_reference lazy_t
-val coq_sumbool_ref : global_reference lazy_t
-val coq_sig_ref : global_reference lazy_t
-
-val coq_or_ref : global_reference lazy_t
-val coq_iff_ref : global_reference lazy_t
+val build_coq_ex : GlobRef.t delayed
+
+val coq_eq_ref : GlobRef.t lazy_t
+val coq_identity_ref : GlobRef.t lazy_t
+val coq_jmeq_ref : GlobRef.t lazy_t
+val coq_eq_true_ref : GlobRef.t lazy_t
+val coq_existS_ref : GlobRef.t lazy_t
+val coq_existT_ref : GlobRef.t lazy_t
+val coq_exist_ref : GlobRef.t lazy_t
+val coq_not_ref : GlobRef.t lazy_t
+val coq_False_ref : GlobRef.t lazy_t
+val coq_sumbool_ref : GlobRef.t lazy_t
+val coq_sig_ref : GlobRef.t lazy_t
+
+val coq_or_ref : GlobRef.t lazy_t
+val coq_iff_ref : GlobRef.t lazy_t
diff --git a/library/global.mli b/library/global.mli
index 015f4d582..906d246ee 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -123,26 +123,26 @@ val env_of_context : Environ.named_context_val -> Environ.env
 val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 val is_joined_environment : unit -> bool
 
-val is_polymorphic : Globnames.global_reference -> bool
-val is_template_polymorphic : Globnames.global_reference -> bool
-val is_type_in_type : Globnames.global_reference -> bool
+val is_polymorphic : GlobRef.t -> bool
+val is_template_polymorphic : GlobRef.t -> bool
+val is_type_in_type : GlobRef.t -> bool
 
 val constr_of_global_in_context : Environ.env ->
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 val type_of_global_in_context : Environ.env -> 
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.AUContext.t
+val universes_of_global : GlobRef.t -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
diff --git a/library/globnames.ml b/library/globnames.ml
index 2fa3adba2..6b78d12ba 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Mod_subst
 open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
-type global_reference = Names.global_reference =
+type global_reference = GlobRef.t =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
@@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false
 let isIndRef = function IndRef _ -> true | _ -> false
 let isConstructRef = function ConstructRef _ -> true | _ -> false
 
-let eq_gr gr1 gr2 =
-  gr1 == gr2 || match gr1,gr2 with
-    | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2
-    | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
-    | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-    | VarRef v1, VarRef v2 -> Id.equal v1 v2
-    | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
-
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
@@ -245,3 +237,6 @@ let pop_global_reference = function
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
+
+(* Deprecated *)
+let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index f2b88b870..2fe35ebcc 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -14,71 +14,73 @@ open Constr
 open Mod_subst
 
 (** {6 Global reference is a kernel side type for all references together } *)
-type global_reference = Names.global_reference =
+type global_reference = GlobRef.t =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
   | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+[@@ocaml.deprecated "Use Names.GlobRef.t"]
 
-val isVarRef : global_reference -> bool
-val isConstRef : global_reference -> bool
-val isIndRef : global_reference -> bool
-val isConstructRef : global_reference -> bool
+val isVarRef : GlobRef.t -> bool
+val isConstRef : GlobRef.t -> bool
+val isIndRef : GlobRef.t -> bool
+val isConstructRef : GlobRef.t -> bool
 
-val eq_gr : global_reference -> global_reference -> bool
-val canonical_gr : global_reference -> global_reference
+val eq_gr : GlobRef.t -> GlobRef.t -> bool
+[@@ocaml.deprecated "Use Names.GlobRef.equal"]
+val canonical_gr : GlobRef.t -> GlobRef.t
 
-val destVarRef : global_reference -> variable
-val destConstRef : global_reference -> Constant.t
-val destIndRef : global_reference -> inductive
-val destConstructRef : global_reference -> constructor
+val destVarRef : GlobRef.t -> variable
+val destConstRef : GlobRef.t -> Constant.t
+val destIndRef : GlobRef.t -> inductive
+val destConstructRef : GlobRef.t -> constructor
 
-val is_global : global_reference -> constr -> bool
+val is_global : GlobRef.t -> constr -> bool
 
 val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> global_reference -> global_reference * constr
-val subst_global_reference : substitution -> global_reference -> global_reference
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
 (** This constr is not safe to be typechecked, universe polymorphism is not 
     handled here: just use for printing *)
-val printable_constr_of_global : global_reference -> constr
+val printable_constr_of_global : GlobRef.t -> constr
 
 (** Turn a construction denoting a global reference into a global reference;
    raise [Not_found] if not a global reference *)
-val global_of_constr : constr -> global_reference
+val global_of_constr : constr -> GlobRef.t
 
 (** Obsolete synonyms for constr_of_global and global_of_constr *)
-val reference_of_constr : constr -> global_reference
+val reference_of_constr : constr -> GlobRef.t
 [@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
 
 module RefOrdered : sig
-  type t = global_reference
+  type t = GlobRef.t
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val hash : t -> int
 end
 
 module RefOrdered_env : sig
-  type t = global_reference
+  type t = GlobRef.t
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val hash : t -> int
 end
 
-module Refset : CSig.SetS with type elt = global_reference
+module Refset : CSig.SetS with type elt = GlobRef.t
 module Refmap : Map.ExtS
-  with type key = global_reference and module Set := Refset
+  with type key = GlobRef.t and module Set := Refset
 
-module Refset_env : CSig.SetS with type elt = global_reference
+module Refset_env : CSig.SetS with type elt = GlobRef.t
 module Refmap_env : Map.ExtS
-  with type key = global_reference and module Set := Refset_env
+  with type key = GlobRef.t and module Set := Refset_env
 
 (** {6 Extended global references } *)
 
 type syndef_name = KerName.t
 
 type extended_global_reference =
-  | TrueGlobal of global_reference
+  | TrueGlobal of GlobRef.t
   | SynDef of syndef_name
 
 module ExtRefOrdered : sig
@@ -89,7 +91,7 @@ module ExtRefOrdered : sig
 end
 
 type global_reference_or_constr = 
-  | IsGlobal of global_reference
+  | IsGlobal of GlobRef.t
   | IsConstr of constr
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
@@ -100,7 +102,6 @@ val encode_con : DirPath.t -> Id.t -> Constant.t
 val decode_con : Constant.t -> DirPath.t * Id.t
 
 (** {6 Popping one level of section in global names } *)
-
 val pop_con : Constant.t -> Constant.t
 val pop_kn : MutInd.t-> MutInd.t
-val pop_global_reference : global_reference -> global_reference
+val pop_global_reference : GlobRef.t -> GlobRef.t
diff --git a/library/keys.ml b/library/keys.ml
index 34a6adabe..89363455d 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -10,12 +10,13 @@
 
 (** Keys for unification and indexing *)
 
-open Globnames
+open Names
 open Term
+open Globnames
 open Libobject
 
 type key =
-  | KGlob of global_reference
+  | KGlob of GlobRef.t
   | KLam
   | KLet
   | KProd
@@ -126,7 +127,7 @@ let constr_key kind c =
       | Construct (c,u) -> KGlob (ConstructRef c)
       | Var id -> KGlob (VarRef id)
       | App (f, _) -> aux f
-      | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p))
+      | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
       | Cast (p, _, _) -> aux p
       | Lambda _ -> KLam 
       | Prod _ -> KProd
diff --git a/library/keys.mli b/library/keys.mli
index 1fb9a3de0..198383650 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Globnames
-
 type key
 
 val declare_equiv_keys : key -> key -> unit
@@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool
 val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
-val pr_keys : (global_reference -> Pp.t) -> Pp.t
+val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t
 (** Pretty-print the mapping *)
diff --git a/library/lib.mli b/library/lib.mli
index 26f1718cc..1d77212e9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-
+open Names
 (** Lib: record of operations, backtrack, low-level sections *)
 
 (** This module provides a general mechanism to keep a trace of all operations
@@ -28,7 +28,7 @@ type node =
 
 and library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (Names.Id.t * Libobject.obj) list
+type lib_objects = (Id.t * Libobject.obj) list
 
 (** {6 Object iteration functions. } *)
 
@@ -54,13 +54,13 @@ val segment_of_objects :
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
+val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
+val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name
 
 (** {6 ... } *)
 
@@ -76,15 +76,15 @@ val contents_after : Libnames.object_name -> library_segment
 (** {6 Functions relative to current path } *)
 
 (** User-side names *)
-val cwd : unit -> Names.DirPath.t
-val cwd_except_section : unit -> Names.DirPath.t
-val current_dirpath : bool -> Names.DirPath.t (* false = except sections *)
-val make_path : Names.Id.t -> Libnames.full_path
-val make_path_except_section : Names.Id.t -> Libnames.full_path
+val cwd : unit -> DirPath.t
+val cwd_except_section : unit -> DirPath.t
+val current_dirpath : bool -> DirPath.t (* false = except sections *)
+val make_path : Id.t -> Libnames.full_path
+val make_path_except_section : Id.t -> Libnames.full_path
 
 (** Kernel-side names *)
-val current_mp : unit -> Names.ModPath.t
-val make_kn : Names.Id.t -> Names.KerName.t
+val current_mp : unit -> ModPath.t
+val make_kn : Id.t -> KerName.t
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -97,19 +97,19 @@ val is_modtype : unit -> bool
    if the latest module started is a module type.  *)
 val is_modtype_strict : unit -> bool
 val is_module : unit -> bool
-val current_mod_id : unit -> Names.module_ident
+val current_mod_id : unit -> module_ident
 
 (** Returns the opening node of a given name *)
-val find_opening_node : Names.Id.t -> node
+val find_opening_node : Id.t -> node
 
 (** {6 Modules and module types } *)
 
 val start_module :
-  export -> Names.module_ident -> Names.ModPath.t ->
+  export -> module_ident -> ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val start_modtype :
-  Names.module_ident -> Names.ModPath.t ->
+  module_ident -> ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val end_module :
@@ -124,23 +124,23 @@ val end_modtype :
 
 (** {6 Compilation units } *)
 
-val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
-val end_compilation_checks : Names.DirPath.t -> Libnames.object_name
+val start_compilation : DirPath.t -> ModPath.t -> unit
+val end_compilation_checks : DirPath.t -> Libnames.object_name
 val end_compilation :
   Libnames.object_name-> Libnames.object_prefix * library_segment
 
 (** The function [library_dp] returns the [DirPath.t] of the current
    compiling library (or [default_library]) *)
-val library_dp : unit -> Names.DirPath.t
+val library_dp : unit -> DirPath.t
 
 (** Extract the library part of a name even if in a section *)
-val dp_of_mp : Names.ModPath.t -> Names.DirPath.t
-val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
-val library_part :  Globnames.global_reference -> Names.DirPath.t
+val dp_of_mp : ModPath.t -> DirPath.t
+val split_modpath : ModPath.t -> DirPath.t * Id.t list
+val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : Names.Id.t -> unit
+val open_section : Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
@@ -164,31 +164,31 @@ type abstr_info = private {
   (** Universe quantification, same length as the substitution *)
 }
 
-val instance_from_variable_context : variable_context -> Names.Id.t array
+val instance_from_variable_context : variable_context -> Id.t array
 val named_of_variable_context : variable_context -> Context.Named.t
 
-val section_segment_of_constant : Names.Constant.t -> abstr_info
-val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info
-val section_segment_of_reference : Globnames.global_reference -> abstr_info
+val section_segment_of_constant : Constant.t -> abstr_info
+val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
+val section_segment_of_reference : GlobRef.t -> abstr_info
 
-val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
+val variable_section_segment_of_reference : GlobRef.t -> variable_context
 
-val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array
-val is_in_section : Globnames.global_reference -> bool
+val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
+val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Names.Constant.t -> Context.Named.t -> unit
+  Constant.t -> Context.Named.t -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  Names.MutInd.t -> Context.Named.t -> unit
+  MutInd.t -> Context.Named.t -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
-val discharge_kn :  Names.MutInd.t -> Names.MutInd.t
-val discharge_con : Names.Constant.t -> Names.Constant.t
-val discharge_global : Globnames.global_reference -> Globnames.global_reference
-val discharge_inductive : Names.inductive -> Names.inductive
+val discharge_kn :  MutInd.t -> MutInd.t
+val discharge_con : Constant.t -> Constant.t
+val discharge_global : GlobRef.t -> GlobRef.t
+val discharge_inductive : inductive -> inductive
 val discharge_abstract_universe_context :
   abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/library/nametab.mli b/library/nametab.mli
index cd28518ab..2ec73a986 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -75,7 +75,7 @@ val error_global_not_found : qualid CAst.t -> 'a
 
 type visibility = Until of int | Exactly of int
 
-val push : visibility -> full_path -> global_reference -> unit
+val push : visibility -> full_path -> GlobRef.t -> unit
 val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
@@ -91,7 +91,7 @@ val push_universe : visibility -> full_path -> universe_id -> unit
 (** These functions globalize a (partially) qualified name or fail with
    [Not_found] *)
 
-val locate : qualid -> global_reference
+val locate : qualid -> GlobRef.t
 val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> Constant.t
 val locate_syndef : qualid -> syndef_name
@@ -105,20 +105,20 @@ val locate_universe : qualid -> universe_id
    references, like [locate] and co, but raise a nice error message
    in case of failure *)
 
-val global : reference -> global_reference
+val global : reference -> GlobRef.t
 val global_inductive : reference -> inductive
 
 (** These functions locate all global references with a given suffix;
    if [qualid] is valid as such, it comes first in the list *)
 
-val locate_all : qualid -> global_reference list
+val locate_all : qualid -> GlobRef.t list
 val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
 (** Mapping a full path to a global reference *)
 
-val global_of_path : full_path -> global_reference
+val global_of_path : full_path -> GlobRef.t
 val extended_global_of_path : full_path -> extended_global_reference
 
 (** {6 These functions tell if the given absolute name is already taken } *)
@@ -144,7 +144,7 @@ val full_name_module : qualid -> DirPath.t
    definition, and the (full) dirpath associated to a module path *)
 
 val path_of_syndef : syndef_name -> full_path
-val path_of_global : global_reference -> full_path
+val path_of_global : GlobRef.t -> full_path
 val dirpath_of_module : ModPath.t -> DirPath.t
 val path_of_modtype : ModPath.t -> full_path
 
@@ -155,12 +155,12 @@ val path_of_universe : universe_id -> full_path
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
-val dirpath_of_global : global_reference -> DirPath.t
-val basename_of_global : global_reference -> Id.t
+val dirpath_of_global : GlobRef.t -> DirPath.t
+val basename_of_global : GlobRef.t -> Id.t
 
 (** Printing of global references using names as short as possible.
     @raise Not_found when the reference is not in the global tables. *)
-val pr_global_env : Id.Set.t -> global_reference -> Pp.t
+val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
 
 
 (** The [shortest_qualid] functions given an object with [user_name]
@@ -168,7 +168,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t
    Coq.A.B.x that denotes the same object.
    @raise Not_found for unknown objects. *)
 
-val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
+val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ModPath.t -> qualid
 val shortest_qualid_of_module : ModPath.t -> qualid
@@ -177,7 +177,7 @@ val shortest_qualid_of_universe : universe_id -> qualid
 (** Deprecated synonyms *)
 
 val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
-val absolute_reference : full_path -> global_reference (** = global_of_path *)
+val absolute_reference : full_path -> GlobRef.t (** = global_of_path *)
 
 (** {5 Generic name handling} *)