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

25 files changed, 57 insertions, 72 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 4d09e879d..4c4ba980d 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 
 let pr_dirpath dp = str (Dir_path.to_string dp)
-let default_root_prefix = Dir_path.make []
+let default_root_prefix = Dir_path.empty
 let split_dirpath d =
   let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
 let extend_dirpath p id = Dir_path.make (id :: Dir_path.repr p)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a07b6aa69..bb3eeb2e0 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -42,7 +42,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
-      Dir_path.equal dir Dir_path.empty && Id.equal id (basename sp)
+      Dir_path.is_empty dir && Id.equal id (basename sp)
   | _ ->
       false
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index cfb704932..9a27ff2a3 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -837,7 +837,8 @@ let sort_universes orig =
 (* Temporary inductive type levels *)
 
 let fresh_level =
-  let n = ref 0 in fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.make [])
+  let n = ref 0 in
+  fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.empty)
 
 let fresh_local_univ () = Atom (fresh_level ())
 
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")
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 850234c3b..69e22da43 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -460,7 +460,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
     match wf_rel_expr_opt with 
       | None ->
 	  let ltof =
-	    let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) in
+	    let make_dir l = Dir_path.make (List.rev_map Id.of_string l) in
 	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a041205bf..e89e2f894 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -132,9 +132,8 @@ let coq_constant s =
     Coqlib.init_modules s;;
 
 let find_reference sl s =
-    (Nametab.locate (make_qualid(Names.Dir_path.make
-			   (List.map Id.of_string (List.rev sl)))
-	       (Id.of_string s)));;
+  let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in
+  Nametab.locate (make_qualid dp (Id.of_string s))
 
 let eq = lazy(coq_constant "eq")
 let refl_equal = lazy(coq_constant "eq_refl")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8816d960f..addce6b1c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -50,10 +50,8 @@ let coq_base_constant s =
     (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
 
 let find_reference sl s =
-    (locate (make_qualid(Names.Dir_path.make
-			   (List.map Id.of_string (List.rev sl)))
-	       (Id.of_string s)));;
-
+  let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in
+  locate (make_qualid dp (Id.of_string s))
 
 let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
@@ -84,11 +82,8 @@ let type_of_const t =
     |_ -> assert false
 
 
-let constant sl s =
-  constr_of_global
-    (locate (make_qualid(Names.Dir_path.make
-			   (List.map Id.of_string (List.rev sl)))
-	       (Id.of_string s)));;
+let constant sl s = constr_of_global (find_reference sl s)
+
 let const_of_ref = function
     ConstRef kn -> kn
   | _ -> anomaly (Pp.str "ConstRef expected")
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 3bb57a3b3..6cfac9605 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -247,11 +247,11 @@ let my_constant c =
 let new_ring_path =
   Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (Label.make s))
+  lazy(make_kn (MPfile new_ring_path) Dir_path.empty (Label.make s))
 let znew_ring_path =
   Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (Label.make s))
+  lazy(make_kn (MPfile znew_ring_path) Dir_path.empty (Label.make s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -830,7 +830,7 @@ let new_field_path =
   Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (Label.make s))
+  lazy(make_kn (MPfile new_field_path) Dir_path.empty (Label.make s))
 
 
 let _ = add_map "field"
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 601a4ffd1..fc64da58e 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -16,7 +16,7 @@ open Coqlib
 
 exception Non_closed_ascii
 
-let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
 let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 643dacbab..ef4636699 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -9,18 +9,19 @@
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
+open Names
 open Globnames
 open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.Dir_path.make (List.map Names.Id.of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id)
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
-let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.Label.make id)
-let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
+let make_mind mp id = Names.make_mind mp Dir_path.empty (Label.make id)
+let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
-  let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.Label.make modname)
+  let mp = MPdot (MPfile (make_dir dir), Label.make modname)
   in make_mind mp id
 
 
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index d84fad6ff..055b99adc 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -19,7 +19,7 @@ exception Non_closed_number
 open Glob_term
 open Bigint
 
-let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
 let make_path dir id = Libnames.make_path dir (Id.of_string id)
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index d583f44cb..ca02f61b7 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -23,7 +23,7 @@ open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
 
-let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let positive_path = make_path binnums "positive"
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 864f35e80..fcd01569a 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -20,7 +20,7 @@ let cprop =
   N.make_con
    (N.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
-   (N.Dir_path.make [])
+   (N.Dir_path.empty)
    (N.Label.make "CProp")
 ;;
 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 43175e80c..1201ff8e0 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Term
 
-let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 3a5cb784e..0264f67fa 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -331,7 +331,7 @@ let print_located_qualid ref =
   match List.map expand (N.locate_extended_all qid) with
     | [] ->
 	let (dir,id) = repr_qualid qid in
-	if dir = Dir_path.empty then
+	if Dir_path.is_empty dir then
 	  str "No object of basename " ++ pr_id id
 	else
 	  str "No object of suffix " ++ pr_qualid qid
@@ -634,7 +634,7 @@ let print_any_name = function
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
-    if (Dir_path.repr dir) <> [] then raise Not_found;
+    if not (Dir_path.is_empty dir) then raise Not_found;
     let (_,c,typ) = Global.lookup_named str in
     (print_named_decl (str,c,typ))
   with Not_found ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5980dae0c..c9341eead 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -208,7 +208,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
-    dir = Dir_path.empty ||
+    Dir_path.is_empty dir ||
     try
       match Nametab.locate_dir (qualid_of_dirpath dir) with
 	  DirOpenModtype _ -> false
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 6b2f02f41..8b0820c52 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -52,7 +52,7 @@ let proper_proxy_class =
 
 let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
 
-let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.rev_map Id.of_string l)
 
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6e3cc1117..8ba105657 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -55,7 +55,7 @@ let set_batch_mode () = batch_mode := true
 let toplevel_default_name = Dir_path.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
-  if Dir_path.equal dir Dir_path.empty then error "Need a non empty toplevel module name";
+  if Dir_path.is_empty dir then error "Need a non empty toplevel module name";
   toplevel_name := Some dir
 let unset_toplevel_name () = toplevel_name := None
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4052ac82..4287db520 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -400,7 +400,7 @@ let print_located_module r =
     let dir = Nametab.full_name_module qid in
     msg_notice (str "Module " ++ pr_dirpath dir)
   with Not_found ->
-    if Dir_path.equal (fst (repr_qualid qid)) Dir_path.empty then
+    if Dir_path.is_empty (fst (repr_qualid qid)) then
       msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid)
     else
       msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid)