Nicer code concerning dirpaths and modpath around Lib

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

4 files changed, 9 insertions, 13 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7fffc960bc..f57832d3f6 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -52,7 +52,7 @@ let toplevel_env () =
 
 let environment_until dir_opt =
   let rec parse = function
-    | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
+    | [] when dir_opt = None -> [Lib.current_mp (), toplevel_env ()]
     | [] -> []
     | d :: l ->
       let meb =
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 659ee4ec4b..0903f85a04 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1301,9 +1301,8 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  match DirPath.repr (dirpath_of_string s) with
-    | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id)
-    | [] -> assert false
+  let d, id = Libnames.split_dirpath (dirpath_of_string s) in
+  Constant.make2 (MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2109ba632f..66acf23edc 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -58,18 +58,16 @@ let raw_string_of_modfile = function
   | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
-let current_toplevel () = fst (Lib.current_prefix ())
-
 let is_toplevel mp =
-  mp = initial_path || mp = current_toplevel ()
+  ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let mp_length mp =
-  let mp0 = current_toplevel () in
+  let mp0 = Lib.current_mp () in
   let rec len = function
-    | mp when mp = mp0 -> 1
+    | mp when ModPath.equal mp mp0 -> 1
     | MPdot (mp,_) -> 1 + len mp
     | _ -> 1
   in len mp
@@ -97,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
   | mp -> mp,ll
 
 let labels_of_ref r =
-  let mp_top = current_toplevel () in
+  let mp_top = Lib.current_mp () in
   let mp,_,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
@@ -419,8 +417,8 @@ let error_non_implicit msg =
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
-	match base_mp (current_toplevel ()) with
-	  | MPfile dp' when dp<>dp' ->
+	match base_mp (Lib.current_mp ()) with
+	  | MPfile dp' when not (DirPath.equal dp dp') ->
 	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
 	  | _ -> ()
       end
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index ce6f8e229e..91d2531dd2 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -49,7 +49,6 @@ val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
 val repr_of_r : global_reference -> module_path * DirPath.t * Label.t
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> Label.t
-val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
 val string_of_modfile : module_path -> string