Revert copy/pasted function in to minilib thanks to clib.cma

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

14 files changed, 67 insertions, 299 deletions

diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 57699c686..fe790042b 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -10,7 +10,6 @@
 
   open Lexing
   open Format
-  open Minilib
 
   let string_buffer = Buffer.create 1024
 
@@ -23,7 +22,7 @@ let ignore = space | ('#' [^ '\n']*)
 
 rule prefs m = parse
   |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
-				 prefs (Stringmap.add id conf m) lexbuf }
+				 prefs (Util.Stringmap.add id conf m) lexbuf }
   | _     { let c = lexeme_start lexbuf in
 	      eprintf "coqiderc: invalid character (%d)\n@." c;
 	      prefs m lexbuf }
@@ -48,7 +47,7 @@ and string = parse
   let load_file f =
     let c = open_in f in
     let lb = from_channel c in
-    let m = prefs Stringmap.empty lb in
+    let m = prefs Util.Stringmap.empty lb in
     close_in c;
     m
 
@@ -59,7 +58,7 @@ and string = parse
       | [] -> ()
       | s :: sl -> fprintf fmt "%S@ %a" s print_list sl
     in
-    Stringmap.iter
+    Util.Stringmap.iter
       (fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
     fprintf fmt "@.";
     close_out c
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f44b8a5e3..6e3c85d47 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1419,7 +1419,7 @@ let do_print session =
       let print_button  = GButton.button ~stock:`PRINT  ~label:"Print"  ~packing:hbox_print#add () in
       let callback_print () =
         let cmd = print_entry#text in
-        let s,_ = run_command av#insert_message cmd in
+        let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in
         flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
         print_window#destroy ()
       in
@@ -1429,11 +1429,11 @@ let do_print session =
     end
 
 let load_file handler f =
-  let f = absolute_filename f in
+  let f = CUnix.correct_path f (Sys.getcwd ()) in
   try
     prerr_endline "Loading file starts";
-    let is_f = Minilib.same_file f in
-      if not (Minilib.list_fold_left_i
+    let is_f = CUnix.same_file f in
+      if not (Util.list_fold_left_i
 		(fun i found x -> if found then found else
                    let {analyzed_view=av} = x in
                      (match av#filename with
@@ -1549,7 +1549,7 @@ let main files =
   (try
      let icon_image = Filename.concat (List.find
        (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-       Minilib.xdg_data_dirs) "coq.png" in
+       (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in
      let icon = GdkPixbuf.from_file icon_image in
      w#set_icon (Some icon)
    with _ -> ());
@@ -1650,7 +1650,7 @@ let main files =
           local_cd f ^ current.cmd_coqdoc ^ " --" ^ kind ^
 	    " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
         in
-        let s,_ = run_command av#insert_message cmd in
+        let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in
         flash_info (cmd ^
                       if s = Unix.WEXITED 0
                       then " succeeded"
@@ -1769,7 +1769,7 @@ let main files =
 	let cmd = current.cmd_coqc ^ " -I "
 	  ^ (Filename.quote (Filename.dirname f))
 	  ^ " " ^ (Filename.quote f) in
-	let s,res = run_command av#insert_message cmd in
+	let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in
 	if s = Unix.WEXITED 0 then
 	  flash_info (f ^ " successfully compiled")
 	else begin
@@ -1792,7 +1792,7 @@ let main files =
 	  save_f ();
 	*)
 	av#insert_message "Command output:\n";
-	let s,res = run_command av#insert_message cmd in
+	let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in
 	last_make := res;
 	last_make_index := 0;
 	flash_info (current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
@@ -1839,7 +1839,7 @@ let main files =
 	flash_info "Cannot make makefile: this buffer has no name"
       | Some f ->
 	let cmd = local_cd f ^ current.cmd_coqmakefile in
-	let s,res = run_command av#insert_message cmd in
+	let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in
 	flash_info
 	  (current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
@@ -1856,7 +1856,7 @@ let main files =
   let windows_actions = GAction.action_group ~name:"Windows" () in
   let help_actions = GAction.action_group ~name:"Help" () in
   let add_gen_actions menu_name act_grp l =
-    let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x) in
+    let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) in
     let add_simple_template menu_name act_grp text =
       let text' =
 	let l = String.length text - 1 in
@@ -1975,8 +1975,8 @@ let main files =
 	  | None -> warning "Call to external editor available only on named files"
 	  | Some f ->
 	    save_f ();
-	    let com = Minilib.subst_command_placeholder current.cmd_editor (Filename.quote f) in
-	    let _ = run_command av#insert_message com in
+	    let com = Util.subst_command_placeholder current.cmd_editor (Filename.quote f) in
+	    let _ = CUnix.run_command Ideutils.try_convert av#insert_message com in
 	    av#revert) ~stock:`EDIT;
       GAction.add_action "Preferences" ~callback:(fun _ ->
 	begin
@@ -2272,7 +2272,7 @@ let main files =
     (try
        let image = Filename.concat (List.find
 	 (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-	 Minilib.xdg_data_dirs) "coq.png" in
+	 (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in
        let startup_image = GdkPixbuf.from_file image in
        b#insert ~iter:b#start_iter "\n\n";
        b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
@@ -2284,7 +2284,7 @@ let main files =
     (try
        let image = Filename.concat (List.find
 	 (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
-	 Minilib.xdg_data_dirs) "coq.png" in
+	 (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in
        let startup_image = GdkPixbuf.from_file image in
        b#insert ~iter:b#start_iter "\n\n";
        b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
@@ -2367,11 +2367,11 @@ let read_coqide_args argv =
        (output_string stderr "Error: multiple -coqtop options"; exit 1)
     | "-f" :: file :: args ->
 	filter_coqtop coqtop
-	  ((Minilib.canonical_path_name (Filename.dirname file),
+	  ((CUnix.canonical_path_name (Filename.dirname file),
 	    Project_file.read_project_file file) :: project_files) out args
     | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
     | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1
-    | "-debug"::args -> Ideutils.debug := true;
+    | "-debug"::args -> Minilib.debug := true;
       filter_coqtop coqtop project_files ("-debug"::out) args
     | arg::args -> filter_coqtop coqtop project_files (arg::out) args
     | [] -> (coqtop,List.rev project_files,List.rev out)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 4c546ab7f..2dbb3f499 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -34,7 +34,7 @@ let set_win32_path () =
 
 let reroute_stdout_stderr () =
   let out_descr =
-    if !Ideutils.debug then
+    if !Minilib.debug then
       Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log"))
     else
       snd (Unix.pipe ())
@@ -97,7 +97,7 @@ let () =
       try
 	GtkThread.main ()
       with
-	| Sys.Break -> Ideutils.prerr_endline "Interrupted."
+	| Sys.Break -> Minilib.prerr_endline "Interrupted."
 	| e ->
 	    Minilib.safe_prerr_endline
 	      ("CoqIde unexpected error:" ^ (Printexc.to_string e));
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 4ba378b7b..04e1e488d 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -1,6 +1,6 @@
 let ui_m = GAction.ui_manager ();;
 
-let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x)
+let no_under = Util.string_map (fun x -> if x = '_' then '-' else x)
 
 let list_items menu li =
   let res_buf = Buffer.create 500 in
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index cfbeec0b2..569e503c3 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         proof#buffer#insert (goal_str i goals_cnt);
         proof#buffer#insert (g ^ "\n")
       in
-      let () = Minilib.list_fold_left_i fold_goal 2 () rem_goals in
+      let () = Util.list_fold_left_i fold_goal 2 () rem_goals in
 
       ignore(proof#buffer#place_cursor
                ~where:(proof#buffer#end_iter#backward_to_tag_toggle
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 1eb8a41be..3f9bb3aca 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -29,15 +29,8 @@ let set_location = ref  (function s -> failwith "not ready")
 
 let pbar = GRange.progress_bar ~pulse_step:0.2 ()
 
-let debug = ref (false)
-
-let prerr_endline s =
-  if !debug then try prerr_endline s;flush stderr with _ -> ()
-
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 
-let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
-
 let byte_offset_to_char_offset s byte_offset =
   if (byte_offset < String.length s) then begin
     let count_delta = ref 0 in
@@ -282,29 +275,8 @@ let rec print_list print fmt = function
 
 let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
 
-(* TODO: allow to report output as soon as it comes (user-fiendlier
-   for long commands like make...) *)
-let run_command f c =
-  let c = requote c in
-  let result = Buffer.create 127 in
-  let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
-  let buff = String.make 127 ' ' in
-  let buffe = String.make 127 ' ' in
-  let n = ref 0 in
-  let ne = ref 0 in
-  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0
-  do
-    let r = try_convert (String.sub buff 0 !n) in
-    f r;
-    Buffer.add_string result r;
-    let r = try_convert (String.sub buffe 0 !ne) in
-    f r;
-    Buffer.add_string result r
-  done;
-  (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
-
 let browse f url =
-  let com = Minilib.subst_command_placeholder current.cmd_browse url in
+  let com = Util.subst_command_placeholder current.cmd_browse url in
   let _ = Unix.open_process_out com in ()
 (* This beautiful message will wait for twt ...
   if s = 127 then
@@ -324,7 +296,7 @@ let url_for_keyword =
 	let cin =
 	  try let index_urls = Filename.concat (List.find
             (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
-	    Minilib.xdg_config_dirs) "index_urls.txt" in
+	    (Envars.xdg_config_dirs flash_info)) "index_urls.txt" in
 	    open_in index_urls
 	  with Not_found ->
 	    let doc_url = doc_url () in
@@ -353,5 +325,3 @@ let url_for_keyword =
 let browse_keyword f text =
   try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
   with Not_found -> f ("No documentation found for \""^text^"\".\n")
-
-let absolute_filename f = Minilib.correct_path f (Sys.getcwd ())
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index c433d92ac..5aa615549 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -16,7 +16,6 @@ val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
-val debug : bool ref
 val disconnect_revert_timer : unit -> unit
 val disconnect_auto_save_timer : unit -> unit
 val do_convert : string -> string
@@ -25,13 +24,8 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a
 
-val is_char_start : char -> bool
-
 val my_stat : string -> Unix.stats option
 
-(** debug printing *)
-val prerr_endline : string -> unit
-
 val print_id : 'a -> unit
 
 val revert_timer : GMain.Timeout.id option ref
@@ -50,8 +44,6 @@ val stock_to_widget :  ?size:Gtk.Tags.icon_size -> GtkStock.id -> GObj.widget
 open Format
 val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
 
-val run_command : (string -> unit) -> string -> Unix.process_status*string
-
 val custom_coqtop : string option ref
 (* @return command to call coqtop
    - custom_coqtop if set
@@ -69,11 +61,6 @@ val set_location : (string -> unit) ref
 
 val pbar : GRange.progress_bar
 
-(*
-  returns an absolute filename equivalent to given filename
-*)
-val absolute_filename : string -> string
-
 (* In win32, when a command-line is to be executed via cmd.exe
    (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
    quoted "..." zones otherwise some quotes are lost. Solution: we re-quote
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 74a42b234..5638934bd 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -9,109 +9,10 @@
 (** Some excerpt of Util and similar files to avoid loading the whole
     module and its dependencies (and hence Compat and Camlp4) *)
 
-module Stringmap = Map.Make(String)
+let debug = ref (false)
 
-let list_fold_left_i f =
-  let rec it_list_f i a = function
-    | [] -> a
-    | b::l -> it_list_f (i+1) (f i a b) l
-  in
-  it_list_f
-
-(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
-   [l1++l2=l] and [l1] has length [i].
-   It raises [Failure] when [i] is negative or greater than the length of [l]  *)
-
-let list_chop n l =
-  let rec chop_aux i acc = function
-    | tl when i=0 -> (List.rev acc, tl)
-    | h::t -> chop_aux (pred i) (h::acc) t
-    | [] -> failwith "list_chop"
-  in
-  chop_aux n [] l
-
-
-let list_map_i f =
-  let rec map_i_rec i = function
-    | [] -> []
-    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
-  in
-  map_i_rec
-
-
-let list_index x =
-  let rec index_x n = function
-    | y::l -> if x = y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
-
-let list_index0 x l = list_index x l - 1
-
-let list_filter_i p =
-  let rec filter_i_rec i = function
-    | [] -> []
-    | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
-  in
-  filter_i_rec 0
-
-let string_map f s =
-  let l = String.length s in
-  let r = String.create l in
-  for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done;
-  r
-
-let subst_command_placeholder s t =
-  Str.global_replace (Str.regexp_string "%s") t s
-
-(* Split the content of a variable such as $PATH in a list of directories.
-   The separators are either ":" in unix or ";" in win32 *)
-
-let path_to_list = Str.split (Str.regexp "[:;]")
-
-(* On win32, the home directory is probably not in $HOME, but in
-   some other environment variable *)
-
-let home =
-  try Sys.getenv "HOME" with Not_found ->
-    try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
-      try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name
-
-let opt2list = function None -> [] | Some x -> [x]
-
-let (/) = Filename.concat
-
-let coqify d = d / "coq"
-
-let xdg_config_home =
-  coqify (try Sys.getenv "XDG_CONFIG_HOME" with Not_found -> home / ".config")
-
-let relative_base =
-  Filename.dirname (Filename.dirname Sys.executable_name)
-
-let xdg_config_dirs =
-  let sys_dirs =
-    try List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
-    with
-      | Not_found when Sys.os_type = "Win32" -> [relative_base / "config"]
-      | Not_found -> ["/etc/xdg/coq"]
-  in
-  xdg_config_home :: sys_dirs @ opt2list Coq_config.configdir
-
-let xdg_data_home =
-  coqify
-    (try Sys.getenv "XDG_DATA_HOME" with Not_found -> home / ".local" / "share")
-
-let xdg_data_dirs =
-  let sys_dirs =
-    try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
-    with
-      | Not_found when Sys.os_type = "Win32" -> [relative_base / "share"]
-      | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
-  in
-  xdg_data_home :: sys_dirs @ opt2list Coq_config.datadir
-
-let coqtop_path = ref ""
+let prerr_endline s =
+  if !debug then try prerr_endline s;flush stderr with _ -> ()
 
 (* On a Win32 application with no console, writing to stderr raise
    a Sys_error "bad file descriptor", hence the "try" below.
@@ -121,66 +22,3 @@ let coqtop_path = ref ""
 
 let safe_prerr_endline s =
   try prerr_endline s;flush stderr with _ -> ()
-
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p =
-  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
-  let n = String.length curdir in
-  let l = String.length p in
-  if l > n && String.sub p 0 n = curdir then
-    let n' =
-      let sl = String.length Filename.dir_sep in
-      let i = ref n in
-	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
-    remove_path_dot (String.sub p n' (l - n'))
-  else
-    p
-
-let strip_path p =
-  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
-  let n = String.length cwd in
-  let l = String.length p in
-  if l > n && String.sub p 0 n = cwd then
-    let n' =
-      let sl = String.length Filename.dir_sep in
-      let i = ref n in
-	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
-    remove_path_dot (String.sub p n' (l - n'))
-  else
-    remove_path_dot p
-
-let canonical_path_name p =
-  let current = Sys.getcwd () in
-  try
-    Sys.chdir p;
-    let p' = Sys.getcwd () in
-    Sys.chdir current;
-    p'
-  with Sys_error _ ->
-    (* We give up to find a canonical name and just simplify it... *)
-    strip_path p
-
-let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f
-
-(*
-  checks if two file names refer to the same (existing) file by
-  comparing their device and inode.
-  It seems that under Windows, inode is always 0, so we cannot
-  accurately check if
-
-*)
-(* Optimised for partial application (in case many candidates must be
-   compared to f1). *)
-let same_file f1 =
-  try
-    let s1 = Unix.stat f1 in
-    (fun f2 ->
-      try
-        let s2 = Unix.stat f2 in
-        s1.Unix.st_dev = s2.Unix.st_dev &&
-          if Sys.os_type = "Win32" then f1 = f2
-          else s1.Unix.st_ino = s2.Unix.st_ino
-      with
-          Unix.Unix_error _ -> false)
-  with
-      Unix.Unix_error _ -> (fun _ -> false)
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 53d6c87c2..1254f5a6d 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -9,36 +9,10 @@
 (** Some excerpts of Util and similar files to avoid depending on them
     and hence on Compat and Camlp4 *)
 
-module Stringmap : Map.S with type key = string
-
-val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
-val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
-val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list
-val list_chop : int -> 'a list -> 'a list * 'a list
-val list_index0 : 'a -> 'a list -> int
-
-val string_map : (char -> char) -> string -> string
-
-val subst_command_placeholder : string -> string -> string
-
-val home : string
-val xdg_config_home : string
-val xdg_config_dirs : string list
-val xdg_data_home : string
-val xdg_data_dirs : string list
-
-val coqtop_path : string ref
+(** debug printing *)
+val debug : bool ref
+val prerr_endline : string -> unit
 
 (** safe version of Pervasives.prerr_endline
     (avoid exception in win32 without console) *)
 val safe_prerr_endline : string -> unit
-
-val remove_path_dot : string -> string
-val strip_path : string -> string
-val canonical_path_name : string -> string
-(** correct_path f dir = dir/f if f is relative *)
-val correct_path : string -> string -> string
-
-(** checks if two file names refer to the same (existing) file *)
-val same_file : string -> string -> bool
-
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d54bb55d3..27245dd00 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -9,28 +9,28 @@
 open Configwin
 open Printf
 
-let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
-let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
+let pref_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqiderc"
+let accel_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqide.keys"
 let lang_manager = GSourceView2.source_language_manager ~default:true
 let () = lang_manager#set_search_path
-  (Minilib.xdg_data_dirs@lang_manager#search_path)
+  ((Envars.xdg_data_dirs Minilib.prerr_endline)@lang_manager#search_path)
 let style_manager = GSourceView2.source_style_scheme_manager ~default:true
 let () = style_manager#set_search_path
-  (Minilib.xdg_data_dirs@style_manager#search_path)
+  ((Envars.xdg_data_dirs Minilib.prerr_endline)@style_manager#search_path)
 
 let get_config_file name =
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
-  let config_dir = List.find find_config Minilib.xdg_config_dirs in
+  let config_dir = List.find find_config (Envars.xdg_config_dirs Minilib.prerr_endline) in
   Filename.concat config_dir name
 
 (* Small hack to handle v8.3 to v8.4 change in configuration file *)
 let loaded_pref_file =
   try get_config_file "coqiderc"
-  with Not_found -> Filename.concat Minilib.home ".coqiderc"
+  with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqiderc"
 
 let loaded_accel_file =
   try get_config_file "coqide.keys"
-  with Not_found -> Filename.concat Minilib.home ".coqide.keys"
+  with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqide.keys"
 
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
@@ -223,14 +223,14 @@ let current = {
   }
 
 let save_pref () =
-  if not (Sys.file_exists Minilib.xdg_config_home)
-  then Unix.mkdir Minilib.xdg_config_home 0o700;
+  if not (Sys.file_exists (Envars.xdg_config_home Minilib.prerr_endline))
+  then Unix.mkdir (Envars.xdg_config_home Minilib.prerr_endline) 0o700;
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = current in
 
-    let add = Minilib.Stringmap.add in
+    let add = Util.Stringmap.add in
     let (++) x f = f x in
-    Minilib.Stringmap.empty ++
+    Util.Stringmap.empty ++
     add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
@@ -292,7 +292,7 @@ let load_pref () =
 
     let m = Config_lexer.load_file loaded_pref_file in
     let np = current in
-    let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
+    let set k f = try let v = Util.Stringmap.find k m in f v with _ -> () in
     let set_hd k f = set k (fun v -> f (List.hd v)) in
     let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
     let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 6bee0fec1..0a2720c46 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -72,13 +72,13 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | "-custom" :: com :: dependencies :: file :: r ->
     process_cmd_line orig_dir opts (Special (file,dependencies,com) :: l) r
   | "-I" :: d :: r ->
-    process_cmd_line orig_dir opts ((Include (Minilib.correct_path d orig_dir)) :: l) r
+    process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir)) :: l) r
   | "-R" :: p :: lp :: r ->
-    process_cmd_line orig_dir opts (RInclude (Minilib.correct_path p orig_dir,lp) :: l) r
+    process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
   | ("-I"|"-custom") :: _ ->
     raise Parsing_error
   | "-f" :: file :: r ->
-    let file = Minilib.remove_path_dot (Minilib.correct_path file orig_dir) in
+    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match project_file with
       | None -> ()
       | Some _ -> Minilib.safe_prerr_endline
@@ -104,7 +104,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | "-arg" :: a :: r ->
     process_cmd_line orig_dir opts (Arg a :: l) r
   | f :: r ->
-      let f = Minilib.correct_path f orig_dir in
+      let f = CUnix.correct_path f orig_dir in
 	process_cmd_line orig_dir opts ((
           if Filename.check_suffix f ".v" then V f
 	  else if (Filename.check_suffix f ".ml") then ML f
@@ -124,32 +124,32 @@ let rec post_canonize f =
 let split_arguments =
   let rec aux = function
   | V n :: r ->
-	let (v,m,o,s),i,d = aux r in ((Minilib.remove_path_dot n::v,m,o,s),i,d)
+	let (v,m,o,s),i,d = aux r in ((CUnix.remove_path_dot n::v,m,o,s),i,d)
   | ML n :: r ->
       let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,Minilib.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
+      ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
   | MLI n :: r ->
       let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(Minilib.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
+      ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
   | ML4 n :: r ->
       let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,Minilib.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
+      ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
   | MLLIB n :: r ->
       let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,ml,Minilib.remove_path_dot n::mllib,mlpack),o,s),i,d)
+      ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
   | MLPACK n :: r ->
       let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in
-      ((v,(mli,ml4,ml,mllib,Minilib.remove_path_dot n::mlpack),o,s),i,d)
+      ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
   | Special (n,dep,c) :: r ->
       let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,c)::o,s),i,d)
   | Subdir n :: r ->
       let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d)
   | Include p :: r ->
-      let t,(i,r),d = aux r in (t,((Minilib.remove_path_dot (post_canonize p),
-				    Minilib.canonical_path_name p)::i,r),d)
+      let t,(i,r),d = aux r in (t,((CUnix.remove_path_dot (post_canonize p),
+				    CUnix.canonical_path_name p)::i,r),d)
   | RInclude (p,l) :: r ->
-      let t,(i,r),d = aux r in (t,(i,(Minilib.remove_path_dot (post_canonize p),l,
-				      Minilib.canonical_path_name p)::r),d)
+      let t,(i,r),d = aux r in (t,(i,(CUnix.remove_path_dot (post_canonize p),l,
+				      CUnix.canonical_path_name p)::r),d)
   | Def (v,def) :: r ->
       let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs))
   | Arg a :: r ->
@@ -162,9 +162,9 @@ let read_project_file f =
     (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
 
 let args_from_project file project_files default_name =
-  let is_f = Minilib.same_file file in
+  let is_f = CUnix.same_file file in
   let contains_file dir =
-      List.exists (fun x -> is_f (Minilib.correct_path x dir))
+      List.exists (fun x -> is_f (CUnix.correct_path x dir))
   in
   let build_cmd_line i_inc r_inc args =
     List.fold_right (fun (_,i) o -> "-I" :: i :: o) i_inc
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index de2924318..6cd3ef579 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -30,7 +30,7 @@ let version = "1.2";;
 
 let html_config = "Configwin bindings configurator for html parameters"
 
-let home = Minilib.home
+let home = Envars.home ~warn:Minilib.prerr_endline
 
 let mCapture = "Capture";;
 let mType_key = "Type key" ;;
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index e15e1960b..9d1951851 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -55,7 +55,7 @@ class command_window coqtop =
   let remove_cb () =
     let index = notebook#current_page in
     let () = notebook#remove_page index in
-    views := Minilib.list_filter_i (fun i x -> i <> index) !views
+    views := Util.list_filter_i (fun i x -> i <> index) !views
   in
   let _ =
     toolbar#insert_button
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 499d56bd9..048cc6e24 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -16,14 +16,14 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#append_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Minilib.list_chop real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 (* XXX - Temporary hack to compile with archaic lablgtk
   method insert_term ?(build=default_build) ?pos (term:'a) =
     let tab_label,menu_label,page = build term in
     let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Minilib.list_chop real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -32,26 +32,26 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#prepend_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Minilib.list_chop real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
   method set_term (term:'a) =
     let tab_label,menu_label,page = make_page term in
     let real_pos = super#current_page in
-      term_list <- Minilib.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+      term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
       super#set_page ?tab_label ?menu_label page
 
   method get_nth_term i =
     List.nth term_list i
 
   method term_num p =
-    Minilib.list_index0 p term_list
+    Util.list_index0 p term_list
 
   method pages = term_list
 
   method remove_page index =
-    term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+    term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
   method current_term =