Minor code cleanups, especially take advantage of Dir_path.is_empty

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

1 files changed, 2 insertions, 7 deletions

diff --git a/library/library.ml b/library/library.ml
index ea70f17c4..e4e687bec 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -90,7 +90,7 @@ let root_paths_matching_dir_path dir =
 
 let intersections d1 d2 =
   let rec aux d1 =
-    if Dir_path.equal d1 Dir_path.empty then [d2] else
+    if Dir_path.is_empty d1 then [d2] else
       let rest = aux (snd (chop_dirpath 1 d1)) in
       if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
       else rest in
@@ -134,12 +134,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module LibraryOrdered =
-  struct
-    type t = Dir_path.t
-    let compare = Dir_path.compare
-  end
-
+module LibraryOrdered = Dir_path
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)