global_reference migrated from Libnames to new Globnames, less deps in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 278 insertions, 254 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 10e8f3a5d..c386ac6aa 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -13,6 +13,7 @@ open Errors
 open Util
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Term
 open Sign
diff --git a/library/global.ml b/library/global.ml
index e57aea6c9..cb57248b5 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -156,7 +156,7 @@ let import cenv digest =
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-open Libnames
+open Globnames
 
 let type_of_reference env = function
   | VarRef id -> Environ.named_type id env
diff --git a/library/global.mli b/library/global.mli
index 77fd465c8..bd7610ed9 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -98,7 +98,7 @@ val import : compiled_library -> Digest.t -> module_path
 (** Function to get an environment from the constants part of the global
  * environment and a given context. *)
 
-val type_of_global : Libnames.global_reference -> types
+val type_of_global : Globnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
 
diff --git a/library/globnames.ml b/library/globnames.ml
new file mode 100644
index 000000000..ae507de25
--- /dev/null
+++ b/library/globnames.ml
@@ -0,0 +1,174 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Mod_subst
+open Libnames
+
+(*s Global reference is a kernel side type for all references together *)
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+let isVarRef = function VarRef _ -> true | _ -> false
+let isConstRef = function ConstRef _ -> true | _ -> false
+let isIndRef = function IndRef _ -> true | _ -> false
+let isConstructRef = function ConstructRef _ -> true | _ -> false
+
+let eq_gr gr1 gr2 =
+  match gr1,gr2 with
+    | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
+    | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
+    | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
+    | _,_ -> gr1=gr2
+
+let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
+let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
+let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
+let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
+
+let subst_constructor subst ((kn,i),j as ref) =
+  let kn' = subst_ind subst kn in
+    if kn==kn' then ref, mkConstruct ref
+    else ((kn',i),j), mkConstruct ((kn',i),j)
+
+let subst_global subst ref = match ref with
+  | VarRef var -> ref, mkVar var
+  | ConstRef kn ->
+     let kn',t = subst_con subst kn in
+      if kn==kn' then ref, mkConst kn else ConstRef kn', t
+  | IndRef (kn,i) ->
+      let kn' = subst_ind subst kn in
+      if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
+  | ConstructRef ((kn,i),j as c) ->
+      let c',t = subst_constructor subst c in
+	if c'==c then ref,t else ConstructRef c', t
+
+let canonical_gr = function
+  | ConstRef con -> ConstRef(constant_of_kn(canonical_con con))
+  | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i)
+  | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+  | VarRef id -> VarRef id
+
+let global_of_constr c = match kind_of_term c with
+  | Const sp -> ConstRef sp
+  | Ind ind_sp -> IndRef ind_sp
+  | Construct cstr_cp -> ConstructRef cstr_cp
+  | Var id -> VarRef id
+  |  _ -> raise Not_found
+
+let constr_of_global = function
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConst sp
+  | ConstructRef sp -> mkConstruct sp
+  | IndRef sp -> mkInd sp
+
+let constr_of_reference = constr_of_global
+let reference_of_constr = global_of_constr
+
+let global_ord_gen fc fmi x y =
+  let ind_ord (indx,ix) (indy,iy) =
+    let c = Pervasives.compare ix iy in
+    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+  in
+  match x, y with
+    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
+    | IndRef indx, IndRef indy -> ind_ord indx indy
+    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
+      let c = Pervasives.compare jx jy in
+      if c = 0 then ind_ord indx indy else c
+    | _, _ -> Pervasives.compare x y
+
+let global_ord_can = global_ord_gen canonical_con canonical_mind
+let global_ord_user = global_ord_gen user_con user_mind
+
+(* By default, [global_reference] are ordered on their canonical part *)
+
+module RefOrdered = struct
+  type t = global_reference
+  let compare = global_ord_can
+end
+
+module RefOrdered_env = struct
+  type t = global_reference
+  let compare = global_ord_user
+end
+
+module Refset = Set.Make(RefOrdered)
+module Refmap = Map.Make(RefOrdered)
+
+(* Extended global references *)
+
+type syndef_name = kernel_name
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
+
+(* We order [extended_global_reference] via their user part
+   (cf. pretty printer) *)
+
+module ExtRefOrdered = struct
+  type t = extended_global_reference
+  let compare x y =
+    match x, y with
+      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+      | SynDef knx, SynDef kny -> kn_ord knx kny
+      | _, _ -> Pervasives.compare x y
+end
+
+(** {6 Temporary function to brutally form kernel names from section paths } *)
+
+let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
+
+let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
+
+let decode_mind kn =
+  let rec dir_of_mp = function
+    | MPfile dir -> repr_dirpath dir
+    | MPbound mbid ->
+	let _,_,dp = repr_mbid mbid in
+	let id = id_of_mbid mbid in
+	  id::(repr_dirpath dp)
+    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+  in
+  let mp,sec_dir,l = repr_mind kn in
+    if (repr_dirpath sec_dir) = [] then
+     (make_dirpath (dir_of_mp mp)),id_of_label l
+    else
+      anomaly "Section part should be empty!"
+
+let decode_con kn =
+  let mp,sec_dir,l = repr_con kn in
+    match mp,(repr_dirpath sec_dir) with
+	MPfile dir,[] -> (dir,id_of_label l)
+      | _ , [] -> anomaly "MPfile expected!"
+      | _ -> anomaly "Section part should be empty!"
+
+(* popping one level of section in global names *)
+
+let pop_con con =
+  let (mp,dir,l) = repr_con con in
+  Names.make_con mp (pop_dirpath dir) l
+
+let pop_kn kn =
+  let (mp,dir,l) = repr_mind kn in
+  Names.make_mind mp (pop_dirpath dir) l
+
+let pop_global_reference = function
+  | ConstRef con -> ConstRef (pop_con con)
+  | IndRef (kn,i) -> IndRef (pop_kn kn,i)
+  | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
+  | VarRef id -> anomaly "VarRef not poppable"
diff --git a/library/globnames.mli b/library/globnames.mli
new file mode 100644
index 000000000..b41d04970
--- /dev/null
+++ b/library/globnames.mli
@@ -0,0 +1,88 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Mod_subst
+
+(** {6 Global reference is a kernel side type for all references together } *)
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+val isVarRef : global_reference -> bool
+val isConstRef : global_reference -> bool
+val isIndRef : global_reference -> bool
+val isConstructRef : global_reference -> bool
+
+val eq_gr : global_reference -> global_reference -> bool
+val canonical_gr : global_reference -> global_reference
+
+val destVarRef : global_reference -> variable
+val destConstRef : global_reference -> constant
+val destIndRef : global_reference -> inductive
+val destConstructRef : global_reference -> constructor
+
+
+val subst_constructor : substitution -> constructor -> constructor * constr
+val subst_global : substitution -> global_reference -> global_reference * constr
+
+(** Turn a global reference into a construction *)
+val constr_of_global : global_reference -> 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
+
+(** Obsolete synonyms for constr_of_global and global_of_constr *)
+val constr_of_reference : global_reference -> constr
+val reference_of_constr : constr -> global_reference
+
+module RefOrdered : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
+
+module RefOrdered_env : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
+
+module Refset : Set.S with type elt = global_reference
+module Refmap : Map.S with type key = global_reference
+
+(** {6 Extended global references } *)
+
+type syndef_name = kernel_name
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
+
+module ExtRefOrdered : sig
+  type t = extended_global_reference
+  val compare : t -> t -> int
+end
+
+(** {6 Temporary function to brutally form kernel names from section paths } *)
+
+val encode_mind : dir_path -> identifier -> mutual_inductive
+val decode_mind : mutual_inductive -> dir_path * identifier
+val encode_con : dir_path -> identifier -> constant
+val decode_con : constant -> dir_path * identifier
+
+(** {6 Popping one level of section in global names } *)
+
+val pop_con : constant -> constant
+val pop_kn : mutual_inductive-> mutual_inductive
+val pop_global_reference : global_reference -> global_reference
diff --git a/library/heads.ml b/library/heads.ml
index 327b883ee..9ff678fb6 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -14,6 +14,7 @@ open Term
 open Mod_subst
 open Environ
 open Libnames
+open Globnames
 open Nameops
 open Libobject
 open Lib
diff --git a/library/impargs.ml b/library/impargs.ml
index 707b2f4cb..8e9365920 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -9,7 +9,7 @@
 open Errors
 open Util
 open Names
-open Libnames
+open Globnames
 open Term
 open Reduction
 open Declarations
diff --git a/library/impargs.mli b/library/impargs.mli
index 57f1ac71e..0443a6f25 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Libnames
+open Globnames
 open Term
 open Environ
 open Nametab
diff --git a/library/lib.ml b/library/lib.ml
index ff7e9b841..4e2b7437e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open Libnames
+open Globnames
 open Nameops
 open Libobject
 open Summary
diff --git a/library/lib.mli b/library/lib.mli
index 360eada85..318997067 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -132,8 +132,8 @@ val library_dp : unit -> Names.dir_path
 val dp_of_mp : Names.module_path -> Names.dir_path
 val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
 val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
-val library_part :  Libnames.global_reference -> Names.dir_path
-val remove_section_part : Libnames.global_reference -> Names.dir_path
+val library_part :  Globnames.global_reference -> Names.dir_path
+val remove_section_part : Globnames.global_reference -> Names.dir_path
 
 (** {6 Sections } *)
 
@@ -187,8 +187,8 @@ val named_of_variable_context : variable_context -> Sign.named_context
 val section_segment_of_constant : Names.constant -> variable_context
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
 
-val section_instance : Libnames.global_reference -> Names.identifier array
-val is_in_section : Libnames.global_reference -> bool
+val section_instance : Globnames.global_reference -> Names.identifier array
+val is_in_section : Globnames.global_reference -> bool
 
 val add_section_variable : Names.identifier -> Decl_kinds.binding_kind -> unit
 
@@ -201,7 +201,7 @@ val replacement_context : unit ->
 
 val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
-val discharge_global : Libnames.global_reference -> Libnames.global_reference
+val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
 
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 24f083887..37ae97ace 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -10,123 +10,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
-open Term
-open Mod_subst
-
-(*s Global reference is a kernel side type for all references together *)
-type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
-
-let isVarRef = function VarRef _ -> true | _ -> false
-let isConstRef = function ConstRef _ -> true | _ -> false
-let isIndRef = function IndRef _ -> true | _ -> false
-let isConstructRef = function ConstructRef _ -> true | _ -> false
-
-let eq_gr gr1 gr2 =
-  match gr1,gr2 with 
-    | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
-    | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
-    | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
-    | _,_ -> gr1=gr2
-
-let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
-let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
-let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
-let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
-
-let subst_constructor subst ((kn,i),j as ref) =
-  let kn' = subst_ind subst kn in
-    if kn==kn' then ref, mkConstruct ref
-    else ((kn',i),j), mkConstruct ((kn',i),j)
-
-let subst_global subst ref = match ref with
-  | VarRef var -> ref, mkVar var
-  | ConstRef kn ->
-     let kn',t = subst_con subst kn in
-      if kn==kn' then ref, mkConst kn else ConstRef kn', t
-  | IndRef (kn,i) ->
-      let kn' = subst_ind subst kn in
-      if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
-  | ConstructRef ((kn,i),j as c) ->
-      let c',t = subst_constructor subst c in
-	if c'==c then ref,t else ConstructRef c', t
-
-let canonical_gr = function
-  | ConstRef con -> ConstRef(constant_of_kn(canonical_con con))
-  | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i)
-  | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j)
-  | VarRef id -> VarRef id
-
-let global_of_constr c = match kind_of_term c with
-  | Const sp -> ConstRef sp
-  | Ind ind_sp -> IndRef ind_sp
-  | Construct cstr_cp -> ConstructRef cstr_cp
-  | Var id -> VarRef id
-  |  _ -> raise Not_found
-
-let constr_of_global = function
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConst sp
-  | ConstructRef sp -> mkConstruct sp
-  | IndRef sp -> mkInd sp
-
-let constr_of_reference = constr_of_global
-let reference_of_constr = global_of_constr
-
-let global_ord_gen fc fmi x y =
-  let ind_ord (indx,ix) (indy,iy) =
-    let c = Pervasives.compare ix iy in
-    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
-  in
-  match x, y with
-    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
-    | IndRef indx, IndRef indy -> ind_ord indx indy
-    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
-      let c = Pervasives.compare jx jy in
-      if c = 0 then ind_ord indx indy else c
-    | _, _ -> Pervasives.compare x y
-
-let global_ord_can = global_ord_gen canonical_con canonical_mind
-let global_ord_user = global_ord_gen user_con user_mind
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
-  type t = global_reference
-  let compare = global_ord_can
-end
-
-module RefOrdered_env = struct
-  type t = global_reference
-  let compare = global_ord_user
-end
-
-module Refset = Set.Make(RefOrdered)
-module Refmap = Map.Make(RefOrdered)
-
-(* Extended global references *)
-
-type syndef_name = kernel_name
-
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SynDef of syndef_name
-
-(* We order [extended_global_reference] via their user part
-   (cf. pretty printer) *)
-
-module ExtRefOrdered = struct
-  type t = extended_global_reference
-  let compare x y =
-    match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
-      | SynDef knx, SynDef kny -> kn_ord knx kny
-      | _, _ -> Pervasives.compare x y
-end
 
 (**********************************************)
 
@@ -236,32 +119,6 @@ let restrict_path n sp =
   let dir' = list_firstn n (repr_dirpath dir) in
   make_path (make_dirpath dir') s
 
-let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
-
-let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
-
-let decode_mind kn =
-  let rec dir_of_mp = function
-    | MPfile dir -> repr_dirpath dir
-    | MPbound mbid -> 
-	let _,_,dp = repr_mbid mbid in
-	let id = id_of_mbid mbid in
-	  id::(repr_dirpath dp)
-    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
-  in
-  let mp,sec_dir,l = repr_mind kn in
-    if (repr_dirpath sec_dir) = [] then
-     (make_dirpath (dir_of_mp mp)),id_of_label l
-    else
-      anomaly "Section part should be empty!"
-
-let decode_con kn =
-  let mp,sec_dir,l = repr_con kn in
-    match mp,(repr_dirpath sec_dir) with
-	MPfile dir,[] -> (dir,id_of_label l)
-      | _ , [] -> anomaly "MPfile expected!"
-      | _ -> anomaly "Section part should be empty!"
-
 (*s qualified names *)
 type qualid = full_path
 
@@ -295,14 +152,6 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
 
-(*  | ModRef mp ->
-      let mp' = subst_modpath subst mp in if mp==mp' then ref else
-          ModRef mp'
-  | ModTypeRef kn ->
-      let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
-          ModTypeRef kn'
-*)
-
 type reference =
   | Qualid of qualid located
   | Ident of identifier located
@@ -317,28 +166,12 @@ let string_of_reference = function
 
 let pr_reference = function
   | Qualid (_,qid) -> pr_qualid qid
-  | Ident (_,id) -> pr_id id
+  | Ident (_,id) -> str (string_of_id id)
 
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
 
-(* popping one level of section in global names *)
-
-let pop_con con =
-  let (mp,dir,l) = repr_con con in
-  Names.make_con mp (pop_dirpath dir) l
-
-let pop_kn kn =
-  let (mp,dir,l) = repr_mind kn in
-  Names.make_mind mp (pop_dirpath dir) l
-
-let pop_global_reference = function
-  | ConstRef con -> ConstRef (pop_con con)
-  | IndRef (kn,i) -> IndRef (pop_kn kn,i)
-  | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
-  | VarRef id -> anomaly "VarRef not poppable"
-
 (* Deprecated synonyms *)
 
 let make_short_qualid = qualid_of_ident
diff --git a/library/libnames.mli b/library/libnames.mli
index d3eed0364..0fe687343 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -10,69 +10,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Term
-open Mod_subst
-
-(** {6 Global reference is a kernel side type for all references together } *)
-type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
-
-val isVarRef : global_reference -> bool
-val isConstRef : global_reference -> bool
-val isIndRef : global_reference -> bool
-val isConstructRef : global_reference -> bool
-
-val eq_gr : global_reference -> global_reference -> bool
-val canonical_gr : global_reference -> global_reference
-
-val destVarRef : global_reference -> variable
-val destConstRef : global_reference -> constant
-val destIndRef : global_reference -> inductive
-val destConstructRef : global_reference -> constructor
-
-
-val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> global_reference -> global_reference * constr
-
-(** Turn a global reference into a construction *)
-val constr_of_global : global_reference -> 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
-
-(** Obsolete synonyms for constr_of_global and global_of_constr *)
-val constr_of_reference : global_reference -> constr
-val reference_of_constr : constr -> global_reference
-
-module RefOrdered : sig
-  type t = global_reference
-  val compare : global_reference -> global_reference -> int
-end
-
-module RefOrdered_env : sig
-  type t = global_reference
-  val compare : global_reference -> global_reference -> int
-end
-
-module Refset : Set.S with type elt = global_reference
-module Refmap : Map.S with type key = global_reference
-
-(** {6 Extended global references } *)
-
-type syndef_name = kernel_name
-
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SynDef of syndef_name
-
-module ExtRefOrdered : sig
-  type t = extended_global_reference
-  val compare : t -> t -> int
-end
 
 (** {6 Dirpaths } *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
@@ -121,14 +58,6 @@ module Spmap  : Map.S with type key = full_path
 
 val restrict_path : int -> full_path -> full_path
 
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-val encode_mind : dir_path -> identifier -> mutual_inductive
-val decode_mind : mutual_inductive -> dir_path * identifier
-val encode_con : dir_path -> identifier -> constant
-val decode_con : constant -> dir_path * identifier
-
-
 (** {6 ... } *)
 (** A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
@@ -184,12 +113,6 @@ val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
 val loc_of_reference : reference -> loc
 
-(** {6 Popping one level of section in global names } *)
-
-val pop_con : constant -> constant
-val pop_kn : mutual_inductive-> mutual_inductive
-val pop_global_reference : global_reference -> global_reference
-
 (** Deprecated synonyms *)
 
 val make_short_qualid : identifier -> qualid (** = qualid_of_ident *)
diff --git a/library/library.mllib b/library/library.mllib
index edd5bfc07..e3916900f 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,5 +1,6 @@
 Nameops
 Libnames
+Globnames
 Libobject
 Summary
 Nametab
diff --git a/library/nametab.ml b/library/nametab.ml
index 42edb156f..2bdd71cc4 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -12,6 +12,7 @@ open Compat
 open Pp
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Declarations
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 5183abbe8..fe59ffad6 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -11,6 +11,7 @@ open Util
 open Pp
 open Names
 open Libnames
+open Globnames
 
 (** This module contains the tables for globalization. *)