From f6d8fc17dc9474e4d043cf709d672d9259599354 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 Aug 2013 14:30:01 +0000
Subject: 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
---
 plugins/extraction/extract_env.ml |  2 +-
 plugins/extraction/mlutil.ml      |  5 ++---
 plugins/extraction/table.ml       | 14 ++++++--------
 plugins/extraction/table.mli      |  1 -
 plugins/funind/recdef.ml          |  2 +-
 plugins/xml/xmlcommand.ml         |  5 +----
 6 files changed, 11 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7fffc960b..f57832d3f 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 659ee4ec4..0903f85a0 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 2109ba632..66acf23ed 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 ce6f8e229..91d2531dd 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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 857e82fc5..7fbc1b981 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1258,7 +1258,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	  ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
-    let lemma = mkConst (Lib.make_con na) in
+    let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 6145548b2..d065ba61a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -380,10 +380,7 @@ let print internal glob_ref kind xml_library_root =
    match glob_ref with
       Gn.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
-       let kn =
-        let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.Label.of_id id)
-       in
+       let kn = Lib.make_kn id in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Gn.ConstRef kn ->
-- 
cgit v1.2.3