Modulification of dir_path

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

20 files changed, 50 insertions, 50 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3269befdb..bd5e2291a 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -584,7 +584,7 @@ let pp_module mp =
     the constants are directly turned into chars *)
 
 let mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
+  make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (mk_label s)
 
 let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3cd3f7f8a..754016715 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl =
 let rec extract_sfb_spec env mp = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
-      let kn = make_con mp empty_dirpath l in
+      let kn = make_con mp Dir_path.empty l in
       let s = extract_constant_spec env kn cb in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let mind = make_mind mp empty_dirpath l in
+      let mind = make_mind mp Dir_path.empty l in
       let s = Sind (mind, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
@@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function
   | (l,SFBconst cb) :: msb ->
       (try
 	 let vl,recd,msb = factor_fix env l cb msb in
-	 let vc = Array.map (make_con mp empty_dirpath) vl in
+	 let vc = Array.map (make_con mp Dir_path.empty) vl in
 	 let ms = extract_sfb env mp all msb in
 	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
@@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function
 	 else ms
        with Impossible ->
 	 let ms = extract_sfb env mp all msb in
-	 let c = make_con mp empty_dirpath l in
+	 let c = make_con mp Dir_path.empty l in
 	 let b = Visit.needed_con c in
 	 if all || b then
 	   let d = extract_constant env c cb in
@@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function
 	 else ms)
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
-      let mind = make_mind mp empty_dirpath l in
+      let mind = make_mind mp Dir_path.empty l in
       let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (mind, extract_inductive env mind) in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index d8d1d1eae..bcdee5954 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1304,9 +1304,9 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  let null = empty_dirpath in
-  match repr_dirpath (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
+  let null = Dir_path.empty in
+  match Dir_path.repr (dirpath_of_string s) with
+    | id :: d -> make_con (MPfile (Dir_path.make d)) null (label_of_id id)
     | [] -> assert false
 
 let manual_inline_set =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index ca72a38ed..9746c39e4 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp =
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+	let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index b8d75d445..7742dd783 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -650,7 +650,7 @@ and pp_module_type params = function
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in
+      let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c7d8d42de..a54121139 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -56,7 +56,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (Id.to_string (List.hd (repr_dirpath f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (Dir_path.repr f)))
   | _ -> assert false
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -175,7 +175,7 @@ let add_recursors env kn =
     make_con_equiv
       (modpath (user_mind kn))
       (modpath (canonical_mind kn))
-      empty_dirpath (label_of_id id)
+      Dir_path.empty (label_of_id id)
   in
   let mib = Environ.lookup_mind kn env in
   Array.iter
@@ -272,7 +272,7 @@ let safe_pr_long_global r =
     | _ -> assert false
 
 let pr_long_mp mp =
-  let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
+  let lid = Dir_path.repr (Nametab.dirpath_of_module mp) in
   str (String.concat "." (List.map Id.to_string (List.rev lid)))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
@@ -424,7 +424,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (current_toplevel ()) with
 	  | MPfile dp' when dp<>dp' ->
-	      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+	      err (str ("Please load library "^(Dir_path.to_string dp^" first.")))
 	  | _ -> ()
       end
   | _ -> ()
@@ -727,7 +727,7 @@ let string_of_modfile mp =
 
 let file_of_modfile mp =
   let s0 = match mp with
-    | MPfile f -> Id.to_string (List.hd (repr_dirpath f))
+    | MPfile f -> Id.to_string (List.hd (Dir_path.repr f))
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index fbf48889f..2cf3c475e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
-val repr_of_r : global_reference -> module_path * dir_path * label
+val repr_of_r : global_reference -> module_path * Dir_path.t * label
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> label
 val current_toplevel : unit -> module_path
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index f8b1927a3..455f3539b 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -81,8 +81,8 @@ type ineq = Rlt | Rle | Rgt | Rge
 let string_of_R_constant kn =
   match Names.repr_con kn with
     | MPfile dir, sec_dir, id when
-	sec_dir = empty_dirpath &&
-	string_of_dirpath dir = "Coq.Reals.Rdefinitions"
+	sec_dir = Dir_path.empty &&
+	Dir_path.to_string dir = "Coq.Reals.Rdefinitions"
 	-> string_of_label id
     | _ -> "constant_not_of_R"
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f922b2f60..3dfce8bf4 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 = make_dirpath (List.map Id.of_string (List.rev l)) in
+	    let make_dir l = Dir_path.make (List.map Id.of_string (List.rev 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 2d50adf00..5942e11b4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -132,7 +132,7 @@ let coq_constant s =
     Coqlib.init_modules s;;
 
 let find_reference sl s =
-    (Nametab.locate (make_qualid(Names.make_dirpath
+    (Nametab.locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 28752fe4f..68c5e16ae 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -50,7 +50,7 @@ let coq_base_constant s =
     (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
 
 let find_reference sl s =
-    (locate (make_qualid(Names.make_dirpath
+    (locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 
@@ -85,7 +85,7 @@ let type_of_const t =
 
 let constant sl s =
   constr_of_global
-    (locate (make_qualid(Names.make_dirpath
+    (locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 let const_of_ref = function
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 92135d497..11281f114 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -19,7 +19,7 @@ let meaningful_submodule = [ "Z"; "N"; "Pos" ]
 
 let string_of_global r =
   let dp = Nametab.dirpath_of_global r in
-  let prefix = match Names.repr_dirpath dp with
+  let prefix = match Names.Dir_path.repr dp with
     | [] -> ""
     | m::_ ->
       let s = Names.Id.to_string m in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 17ea6f2bf..d02d26007 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -244,13 +244,13 @@ let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (mk_label s))
 let znew_ring_path =
-  make_dirpath (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (mk_label s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -826,10 +826,10 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (mk_label s))
 
 
 let _ = add_map "field"
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 958fdc649..601a4ffd1 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 = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev 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 f86b56bc7..d6b9f73d5 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -14,10 +14,10 @@ open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.make_dirpath (List.map Names.Id.of_string (List.rev l))
+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_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
+let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.mk_label id)
 let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
   let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f7d0091f3..d84fad6ff 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 = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev 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 9faa6edd1..d583f44cb 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 = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev 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/cic2acic.ml b/plugins/xml/cic2acic.ml
index d817396f1..fb951b35f 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -36,7 +36,7 @@ let get_module_path_of_full_path path =
 let remove_module_dirpath_from_dirpath ~basedir dir =
  let module Ln = Libnames in
   if Ln.is_dirpath_prefix_of basedir dir then
-   let ids = Names.repr_dirpath dir in
+   let ids = Names.Dir_path.repr dir in
    let rec remove_firsts n l =
     match n,l with
        (0,l) -> l
@@ -46,11 +46,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
     let ids' =
      List.rev
       (remove_firsts
-        (List.length (Names.repr_dirpath basedir))
+        (List.length (Names.Dir_path.repr basedir))
         (List.rev ids))
     in
      ids'
-  else Names.repr_dirpath dir
+  else Names.Dir_path.repr dir
 ;;
 
 
@@ -61,7 +61,7 @@ let get_uri_of_var v pvars =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = N.make_dirpath modules in
+       let dirpath = N.Dir_path.make modules in
         if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
          modules
         else
@@ -71,7 +71,7 @@ let get_uri_of_var v pvars =
     if List.mem v pvars then
       []
     else
-      search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
+      search_in_open_sections (N.Dir_path.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
@@ -106,21 +106,21 @@ let ext_of_tag =
 exception FunctorsXMLExportationNotImplementedYet;;
 
 let subtract l1 l2 =
- let l1' = List.rev (Names.repr_dirpath l1) in
- let l2' = List.rev (Names.repr_dirpath l2) in
+ let l1' = List.rev (Names.Dir_path.repr l1) in
+ let l2' = List.rev (Names.Dir_path.repr l2) in
   let rec aux =
    function
       he::tl when tl = l2' -> [he]
     | he::tl -> he::(aux tl)
     | [] -> assert (l2' = []) ; []
   in
-   Names.make_dirpath (List.rev (aux l1'))
+   Names.Dir_path.make (List.rev (aux l1'))
 ;;
 
 let token_list_of_path dir id tag =
  let module N = Names in
   let token_list_of_dirpath dirpath =
-   List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in
+   List.rev_map N.Id.to_string (N.Dir_path.repr dirpath) in
   token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 8f1d97d3b..b4ec85ab7 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.make_dirpath [])
+   (N.Dir_path.make [])
    (N.mk_label "CProp")
 ;;
 
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 35760a51d..50309317e 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -46,7 +46,7 @@ let filter_params pvars hyps =
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
-   aux (Names.repr_dirpath modulepath) (List.rev pvars)
+   aux (Names.Dir_path.repr modulepath) (List.rev pvars)
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)
@@ -62,7 +62,7 @@ let search_variables () =
        [] -> []
      | he::tl as modules ->
         let one_section_variables =
-         let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
+         let dirpath = N.Dir_path.make (modules @ N.Dir_path.repr modulepath) in
           let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
@@ -113,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in
+     let toks = List.map N.Id.to_string (N.Dir_path.repr (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.map Names.Id.to_string (List.rev (Names.repr_dirpath dir)))
+    (List.map Names.Id.to_string (List.rev (Names.Dir_path.repr dir)))
 ;;
 
 let _ =
@@ -550,5 +550,5 @@ let _ =
   Library.set_xml_require
     (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
-       (uri_of_dirpath d) (Names.string_of_dirpath d)))
+       (uri_of_dirpath d) (Names.Dir_path.to_string d)))
 ;;