2 files changed, 2 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 7b0078392d..dc665408c9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -84,6 +84,7 @@ module Umap = Map.Make(struct
 type mod_self_id = uniq_ident
 let make_msid = make_uid
 let debug_string_of_msid = string_of_uid
+let id_of_msid (_,s,_) = s
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
diff --git a/kernel/names.mli b/kernel/names.mli
index 31684371d3..0e45778d0a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,6 +48,7 @@ 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 id_of_msid : mod_self_id -> identifier
 val debug_string_of_msid : mod_self_id -> string
 
 (*s Unique names for bound modules *)