Names: remove obsolete mod_self_id

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

2 files changed, 17 insertions, 38 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index d5f301f2f0..aef0039e1f 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -88,15 +88,6 @@ module Umap = Map.Make(struct
 
 type label = string
 
-type mod_self_id = uniq_ident
-let make_msid = make_uid
-let repr_msid (n, id, dp) = (n, id, dp)
-let debug_string_of_msid = debug_string_of_uid
-let refresh_msid (_,s,dir) = make_uid dir s
-let string_of_msid = string_of_uid
-let id_of_msid (_,s,_) = s
-let label_of_msid (_,s,_) = s
-
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
 let repr_mbid (n, id, dp) = (n, id, dp)
@@ -230,7 +221,6 @@ let default_module_name = "If you see this, it's a bug"
 
 let initial_dir = make_dirpath [default_module_name]
 
-let initial_msid = (make_msid initial_dir "If you see this, it's a bug")
 let initial_path = MPfile initial_dir
 
 type variable = identifier
diff --git a/kernel/names.mli b/kernel/names.mli
index b441bf00a9..d64dbe1ca5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -38,26 +38,26 @@ val empty_dirpath : dir_path
 (** Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
+(** {6 Names of structure elements } *)
 
-(** {6 ... } *)
-(** Unique identifier to be used as "self" in structures and
-  signatures - invisible for users *)
 type label
-type mod_self_id
 
-(** The first argument is a file name - to prevent conflict between
-   different files *)
-val make_msid : dir_path -> string -> mod_self_id
-val repr_msid : mod_self_id -> int * string * dir_path
-val id_of_msid : mod_self_id -> identifier
-val label_of_msid : mod_self_id -> label
-val refresh_msid : mod_self_id -> mod_self_id
-val debug_string_of_msid : mod_self_id -> string
-val string_of_msid : mod_self_id -> string
+val mk_label : string -> label
+val string_of_label : label -> string
+
+val label_of_id : identifier -> label
+val id_of_label : label -> identifier
+
+module Labset : Set.S with type elt = label
+module Labmap : Map.S with type key = label
 
 (** {6 Unique names for bound modules } *)
+
 type mod_bound_id
 
+(** The first argument is a file name - to prevent conflict between
+   different files *)
+
 val make_mbid : dir_path -> string -> mod_bound_id
 val repr_mbid : mod_bound_id -> int * string * dir_path
 val id_of_mbid : mod_bound_id -> identifier
@@ -65,18 +65,8 @@ val label_of_mbid : mod_bound_id -> label
 val debug_string_of_mbid : mod_bound_id -> string
 val string_of_mbid : mod_bound_id -> string
 
-(** {6 Names of structure elements } *)
-
-val mk_label : string -> label
-val string_of_label : label -> string
-
-val label_of_id : identifier -> label
-val id_of_label : label -> identifier
-
-module Labset : Set.S with type elt = label
-module Labmap : Map.S with type key = label
-
 (** {6 The module part of the kernel name } *)
+
 type module_path =
   | MPfile of dir_path
   | MPbound of mod_bound_id
@@ -91,13 +81,12 @@ val string_of_mp : module_path -> string
 module MPset : Set.S with type elt = module_path
 module MPmap : Map.S with type key = module_path
 
-(** Name of the toplevel structure *)
-val initial_msid : mod_self_id
-val initial_path : module_path (** [= MPself initial_msid] *)
-
 (** Initial "seed" of the unique identifier generator *)
 val initial_dir : dir_path
 
+(** Name of the toplevel structure *)
+val initial_path : module_path (** [= MPfile initial_dir] *)
+
 (** {6 The absolute names of objects seen by kernel } *)
 
 type kernel_name