Modulification of dir_path

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

7 files changed, 17 insertions, 17 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