4 files changed, 4 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 78d39b6a0..f25e6680d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -127,6 +127,7 @@ module MPord = struct
   let compare = mp_ord
 end
 
+module MPset = Set.Make(MPord)
 module MPmap = Map.Make(MPord)
 
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 89c90fef1..83509075e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -79,6 +79,7 @@ type module_path =
 
 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
 
 
diff --git a/library/libnames.ml b/library/libnames.ml
index e8bdb4818..4440780a5 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -117,6 +117,7 @@ let dirpath_of_string s =
     | dir -> make_dirpath dir
 
 module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
+module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
 
 (*s Section paths are absolute names *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 938be5644..e902cec9b 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -52,6 +52,7 @@ val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
 
 module Dirset : Set.S with type elt = dir_path
+module Dirmap : Map.S with type key = dir_path
 
 (*s Section paths are {\em absolute} names *)
 type section_path