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

7 files changed, 26 insertions, 37 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index aedb81633..c96a9fbc0 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -155,7 +155,7 @@ let _ = Summary.declare_summary "MODULE-INFO"
 
 let mp_of_kn kn =
   let mp,sec,l = repr_kn kn in
-    if Dir_path.equal sec Dir_path.empty then
+    if Dir_path.is_empty sec then
       MPdot (mp,l)
     else
       anomaly (str "Non-empty section in module name!" ++ spc () ++ pr_kn kn)
diff --git a/library/globnames.ml b/library/globnames.ml
index 06a8f823d..e63fa64d5 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -142,6 +142,10 @@ let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id)
 
 let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id)
 
+let check_empty_section dp =
+  if not (Dir_path.is_empty dp) then
+    anomaly (Pp.str "Section part should be empty!")
+
 let decode_mind kn =
   let rec dir_of_mp = function
     | MPfile dir -> Dir_path.repr dir
@@ -152,17 +156,15 @@ let decode_mind kn =
     | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
   let mp,sec_dir,l = repr_mind kn in
-    if (Dir_path.repr sec_dir) = [] then
-     (Dir_path.make (dir_of_mp mp)),Label.to_id l
-    else
-      anomaly (Pp.str "Section part should be empty!")
+  check_empty_section sec_dir;
+  (Dir_path.make (dir_of_mp mp)),Label.to_id l
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
-    match mp,(Dir_path.repr sec_dir) with
-	MPfile dir,[] -> (dir,Label.to_id l)
-      | _ , [] -> anomaly (Pp.str "MPfile expected!")
-      | _ -> anomaly (Pp.str "Section part should be empty!")
+  check_empty_section sec_dir;
+  match mp with
+    | MPfile dir -> (dir,Label.to_id l)
+    | _ -> anomaly (Pp.str "MPfile expected!")
 
 (* popping one level of section in global names *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 01e24f6c7..191b00ea9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -693,38 +693,30 @@ let remove_section_part ref =
 (************************)
 (* Discharging names *)
 
-let pop_kn kn =
-  let (mp,dir,l) = Names.repr_mind kn in
-  Names.make_mind mp (pop_dirpath dir) l
-
-let pop_con con =
-  let (mp,dir,l) = Names.repr_con con in
-  Names.make_con mp (pop_dirpath dir) l
-
 let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
-  not (Names.Dir_path.equal dir Names.Dir_path.empty) &&
+  not (Names.Dir_path.is_empty dir) &&
   Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let defined_in_sec kn =
   let _,dir,_ = Names.repr_mind kn in
-  not (Names.Dir_path.equal dir Names.Dir_path.empty) &&
+  not (Names.Dir_path.is_empty dir) &&
   Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
-      ConstRef (pop_con kn)
+      ConstRef (Globnames.pop_con kn)
   | IndRef (kn,i) when defined_in_sec kn ->
-      IndRef (pop_kn kn,i)
+      IndRef (Globnames.pop_kn kn,i)
   | ConstructRef ((kn,i),j) when defined_in_sec kn ->
-      ConstructRef ((pop_kn kn,i),j)
+      ConstructRef ((Globnames.pop_kn kn,i),j)
   | r -> r
 
 let discharge_kn kn =
-  if defined_in_sec kn then pop_kn kn else kn
+  if defined_in_sec kn then Globnames.pop_kn kn else kn
 
 let discharge_con cst =
-  if con_defined_in_sec cst then pop_con cst else cst
+  if con_defined_in_sec cst then Globnames.pop_con cst else cst
 
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
diff --git a/library/libnames.ml b/library/libnames.ml
index 902222431..9f129793e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -83,7 +83,7 @@ type full_path = {
 
 let eq_full_path p1 p2 =
   Id.equal p1.basename p2.basename &&
-  Int.equal (Dir_path.compare p1.dirpath p2.dirpath) 0
+  Dir_path.equal p1.dirpath p2.dirpath
 
 let make_path pa id = { dirpath = pa; basename = id }
 
@@ -163,8 +163,8 @@ type global_dir_reference =
       (* this won't last long I hope! *)
 
 let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
-  Int.equal (Dir_path.compare d1 d2) 0 &&
-  Int.equal (Dir_path.compare p1 p2) 0 &&
+  Dir_path.equal d1 d2 &&
+  Dir_path.equal p1 p2 &&
   mp_eq mp1 mp2
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
@@ -172,7 +172,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (Dir_path.compare dp1 dp2) 0
+| DirClosedSection dp1, DirClosedSection dp2 -> Dir_path.equal dp1 dp2
 | _ -> false
 
 type reference =
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)
 
diff --git a/library/nameops.ml b/library/nameops.ml
index a8803e7a5..0891d306b 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -142,7 +142,7 @@ let default_library = Names.Dir_path.initial (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
 let coq_root = Id.of_string "Coq"
-let default_root_prefix = Dir_path.make []
+let default_root_prefix = Dir_path.empty
 
 (* Metavariables *)
 let pr_meta = Pp.int
diff --git a/library/nametab.ml b/library/nametab.ml
index 6829e9431..9e0e38745 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -309,7 +309,7 @@ let the_modtypetab = ref (MPTab.empty : mptab)
 module DirPath =
 struct
   type t = Dir_path.t
-  let equal d1 d2 = Int.equal (Dir_path.compare d1 d2) 0
+  let equal = Dir_path.equal
   let to_string = Dir_path.to_string
   let repr dir = match Dir_path.repr dir with
     | [] -> anomaly (Pp.str "Empty dirpath")