lib directory is cut in 2 cma.

 - Clib that does not depend on camlpX and is made to be shared by all coq
   tools/scripts/...
 - Lib that is Coqtop specific

As a side effect for the build system :
 - Coq_config is in Clib and does not appears in makefiles
 - only the BEST version of coqc and coqmktop is made
 - ocamlbuild build system fails latter but is still broken

(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)

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

13 files changed, 36 insertions, 661 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e4cfcb3f71..15916ef8cc 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -30,14 +30,14 @@ let load_rcfile() =
   if !load_rc then
     try
       if !rcfile_specified then
-        if file_readable_p !rcfile then
+        if CUnix.file_readable_p !rcfile then
           Vernac.load_vernac false !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
-      else try let inferedrc = List.find file_readable_p [
-	Envars.xdg_config_home/rcdefaultname^"."^Coq_config.version;
-	Envars.xdg_config_home/rcdefaultname;
-	System.home/"."^rcdefaultname^"."^Coq_config.version;
-	System.home/"."^rcdefaultname;
+      else try let inferedrc = List.find CUnix.file_readable_p [
+	Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname^"."^Coq_config.version;
+	Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname;
+	Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname^"."^Coq_config.version;
+	Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname;
       ] in
         Vernac.load_vernac false inferedrc
 	with Not_found -> ()
@@ -92,9 +92,9 @@ let theories_dirs_map = [
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib () in
+  let coqlib = Envars.coqlib Errors.error in
   let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs in
+  let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
   let dirs = ["states";"plugins"] in
     (* NOTE: These directories are searched from last to first *)
@@ -130,7 +130,7 @@ let init_ocaml_path () =
   let add_subdir dl =
     Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl)
   in
-    Mltop.add_ml_dir (Envars.coqlib ());
+    Mltop.add_ml_dir (Envars.coqlib Errors.error);
     List.iter add_subdir
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bf5c84e647..fe6e350e6e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -20,7 +20,7 @@ open Coqinit
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib () in
+    let coqlib = Envars.coqlib Errors.error in
     let ch = open_in (Filename.concat coqlib "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
@@ -80,7 +80,7 @@ let set_rec_include d p =
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
-  load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
+  load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
 let load_vernacular () =
   List.iter
     (fun (s,b) ->
@@ -261,7 +261,7 @@ let parse_args arglist =
     | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
     | "-coqlib" :: [] -> usage ()
 
-    | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0)
+    | "-where" :: _ -> print_endline (Envars.coqlib Errors.error); exit (if !filter_opts then 2 else 0)
 
     | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0)
 
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
deleted file mode 100644
index d36e466240..0000000000
--- a/toplevel/ide_intf.ml
+++ /dev/null
@@ -1,446 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** * Interface of calls to Coq by CoqIde *)
-
-open Xml_parser
-open Interface
-
-type xml = Xml_parser.xml
-
-(** We use phantom types and GADT to protect ourselves against wild casts *)
-
-type 'a call =
-  | Interp of raw * verbose * string
-  | Rewind of int
-  | Goal
-  | Evars
-  | Hints
-  | Status
-  | GetOptions
-  | SetOptions of (option_name * option_value) list
-  | InLoadPath of string
-  | MkCases of string
-
-(** The actual calls *)
-
-let interp (r,b,s) : string call = Interp (r,b,s)
-let rewind i : int call = Rewind i
-let goals : goals option call = Goal
-let evars : evar list option call = Evars
-let hints : (hint list * hint) option call = Hints
-let status : status call = Status
-let get_options : (option_name * option_state) list call = GetOptions
-let set_options l : unit call = SetOptions l
-let inloadpath s : bool call = InLoadPath s
-let mkcases s : string list list call = MkCases s
-
-(** * Coq answers to CoqIde *)
-
-let abstract_eval_call handler c =
-  try
-    let res = match c with
-      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string)
-      | Rewind i -> Obj.magic (handler.rewind i : int)
-      | Goal -> Obj.magic (handler.goals () : goals option)
-      | Evars -> Obj.magic (handler.evars () : evar list option)
-      | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
-      | Status -> Obj.magic (handler.status () : status)
-      | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
-      | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
-      | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
-      | MkCases s -> Obj.magic (handler.mkcases s : string list list)
-    in Good res
-  with e ->
-    let (l, str) = handler.handle_exn e in
-    Fail (l,str)
-
-(** * XML data marshalling *)
-
-exception Marshal_error
-
-(** Utility functions *)
-
-let massoc x l =
-  try List.assoc x l
-  with Not_found -> raise Marshal_error
-
-let constructor t c args = Element (t, ["val", c], args)
-
-let do_match constr t mf = match constr with
-| Element (s, attrs, args) ->
-  if s = t then
-    let c = massoc "val" attrs in
-    mf c args
-  else raise Marshal_error
-| _ -> raise Marshal_error
-
-let pcdata = function
-| PCData s -> s
-| _ -> raise Marshal_error
-
-let singleton = function
-| [x] -> x
-| _ -> raise Marshal_error
-
-let raw_string = function
-| [] -> ""
-| [PCData s] -> s
-| _ -> raise Marshal_error
-
-let bool_arg tag b = if b then [tag, ""] else []
-
-(** Base types *)
-
-let of_bool b =
-  if b then constructor "bool" "true" []
-  else constructor "bool" "false" []
-
-let to_bool xml = do_match xml "bool"
-  (fun s _ -> match s with
-  | "true" -> true
-  | "false" -> false
-  | _ -> raise Marshal_error)
-
-let of_list f l =
-  Element ("list", [], List.map f l)
-
-let to_list f = function
-| Element ("list", [], l) ->
-  List.map f l
-| _ -> raise Marshal_error
-
-let of_option f = function
-| None -> Element ("option", ["val", "none"], [])
-| Some x -> Element ("option", ["val", "some"], [f x])
-
-let to_option f = function
-| Element ("option", ["val", "none"], []) -> None
-| Element ("option", ["val", "some"], [x]) -> Some (f x)
-| _ -> raise Marshal_error
-
-let of_string s = Element ("string", [], [PCData s])
-
-let to_string = function
-| Element ("string", [], l) -> raw_string l
-| _ -> raise Marshal_error
-
-let of_int i = Element ("int", [], [PCData (string_of_int i)])
-
-let to_int = function
-| Element ("int", [], [PCData s]) -> int_of_string s
-| _ -> raise Marshal_error
-
-let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
-
-let to_pair f g = function
-| Element ("pair", [], [x; y]) -> (f x, g y)
-| _ -> raise Marshal_error
-
-(** More elaborate types *)
-
-let of_option_value = function
-| IntValue i ->
-  constructor "option_value" "intvalue" [of_option of_int i]
-| BoolValue b ->
-  constructor "option_value" "boolvalue" [of_bool b]
-| StringValue s ->
-  constructor "option_value" "stringvalue" [of_string s]
-
-let to_option_value xml = do_match xml "option_value"
-  (fun s args -> match s with
-  | "intvalue" -> IntValue (to_option to_int (singleton args))
-  | "boolvalue" -> BoolValue (to_bool (singleton args))
-  | "stringvalue" -> StringValue (to_string (singleton args))
-  | _ -> raise Marshal_error
-  )
-
-let of_option_state s =
-  Element ("option_state", [], [
-    of_bool s.opt_sync;
-    of_bool s.opt_depr;
-    of_string s.opt_name;
-    of_option_value s.opt_value]
-  )
-
-let to_option_state = function
-| Element ("option_state", [], [sync; depr; name; value]) ->
-  {
-    opt_sync = to_bool sync;
-    opt_depr = to_bool depr;
-    opt_name = to_string name;
-    opt_value = to_option_value value;
-  }
-| _ -> raise Marshal_error
-
-let of_value f = function
-| Good x -> Element ("value", ["val", "good"], [f x])
-| Fail (loc, msg) ->
-  let loc = match loc with
-  | None -> []
-  | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)]
-  in
-  Element ("value", ["val", "fail"] @ loc, [PCData msg])
-
-let to_value f = function
-| Element ("value", attrs, l) ->
-  let ans = massoc "val" attrs in
-  if ans = "good" then Good (f (singleton l))
-  else if ans = "fail" then
-    let loc =
-      try
-        let loc_s = int_of_string (List.assoc "loc_s" attrs) in
-        let loc_e = int_of_string (List.assoc "loc_e" attrs) in
-        Some (loc_s, loc_e)
-      with _ -> None
-    in
-    let msg = raw_string l in
-    Fail (loc, msg)
-  else raise Marshal_error
-| _ -> raise Marshal_error
-
-let of_call = function
-| Interp (raw, vrb, cmd) ->
-  let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
-  Element ("call", ("val", "interp") :: flags, [PCData cmd])
-| Rewind n ->
-  Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
-| Goal ->
-  Element ("call", ["val", "goal"], [])
-| Evars ->
-  Element ("call", ["val", "evars"], [])
-| Hints ->
-  Element ("call", ["val", "hints"], [])
-| Status ->
-  Element ("call", ["val", "status"], [])
-| GetOptions ->
-  Element ("call", ["val", "getoptions"], [])
-| SetOptions opts ->
-  let args = List.map (of_pair (of_list of_string) of_option_value) opts in
-  Element ("call", ["val", "setoptions"], args)
-| InLoadPath file ->
-  Element ("call", ["val", "inloadpath"], [PCData file])
-| MkCases ind ->
-  Element ("call", ["val", "mkcases"], [PCData ind])
-
-let to_call = function
-| Element ("call", attrs, l) ->
-  let ans = massoc "val" attrs in
-  begin match ans with
-  | "interp" ->
-    let raw = List.mem_assoc "raw" attrs in
-    let vrb = List.mem_assoc "verbose" attrs in
-    Interp (raw, vrb, raw_string l)
-  | "rewind" ->
-    let steps = int_of_string (massoc "steps" attrs) in
-    Rewind steps
-  | "goal" -> Goal
-  | "evars" -> Evars
-  | "status" -> Status
-  | "getoptions" -> GetOptions
-  | "setoptions" ->
-    let args = List.map (to_pair (to_list to_string) to_option_value) l in
-    SetOptions args
-  | "inloadpath" -> InLoadPath (raw_string l)
-  | "mkcases" -> MkCases (raw_string l)
-  | "hints" -> Hints
-  | _ -> raise Marshal_error
-  end
-| _ -> raise Marshal_error
-
-let of_status s =
-  let of_so = of_option of_string in
-  let of_sl = of_list of_string in
-  Element ("status", [],
-    [
-      of_sl s.status_path;
-      of_so s.status_proofname;
-      of_sl s.status_allproofs;
-      of_int s.status_statenum;
-      of_int s.status_proofnum;
-    ]
-  )
-
-let to_status = function
-| Element ("status", [], [path; name; prfs; snum; pnum]) ->
-  {
-    status_path = to_list to_string path;
-    status_proofname = to_option to_string name;
-    status_allproofs = to_list to_string prfs;
-    status_statenum = to_int snum;
-    status_proofnum = to_int pnum;
-  }
-| _ -> raise Marshal_error
-
-let of_evar s =
-  Element ("evar", [], [PCData s.evar_info])
-
-let to_evar = function
-| Element ("evar", [], data) -> { evar_info = raw_string data; }
-| _ -> raise Marshal_error
-
-let of_goal g =
-  let hyp = of_list of_string g.goal_hyp in
-  let ccl = of_string g.goal_ccl in
-  Element ("goal", [], [hyp; ccl])
-
-let to_goal = function
-| Element ("goal", [], [hyp; ccl]) ->
-  let hyp = to_list to_string hyp in
-  let ccl = to_string ccl in
-  { goal_hyp = hyp; goal_ccl = ccl }
-| _ -> raise Marshal_error
-
-let of_goals g =
-  let fg = of_list of_goal g.fg_goals in
-  let bg = of_list of_goal g.bg_goals in
-  Element ("goals", [], [fg; bg])
-
-let to_goals = function
-| Element ("goals", [], [fg; bg]) ->
-  let fg = to_list to_goal fg in
-  let bg = to_list to_goal bg in
-  { fg_goals = fg; bg_goals = bg; }
-| _ -> raise Marshal_error
-
-let of_hints =
-  let of_hint = of_list (of_pair of_string of_string) in
-  of_option (of_pair (of_list of_hint) of_hint)
-
-let of_answer (q : 'a call) (r : 'a value) =
-  let convert = match q with
-  | Interp _ -> Obj.magic (of_string : string -> xml)
-  | Rewind _ -> Obj.magic (of_int : int -> xml)
-  | Goal -> Obj.magic (of_option of_goals : goals option -> xml)
-  | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml)
-  | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
-  | Status -> Obj.magic (of_status : status -> xml)
-  | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml)
-  | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
-  | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
-  | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
-  in
-  of_value convert r
-
-let to_answer xml =
-  let rec convert elt = match elt with
-  | Element (tpe, attrs, l) ->
-    begin match tpe with
-    | "unit" -> Obj.magic ()
-    | "string" -> Obj.magic (to_string elt : string)
-    | "int" -> Obj.magic (to_int elt : int)
-    | "status" -> Obj.magic (to_status elt : status)
-    | "bool" -> Obj.magic (to_bool elt : bool)
-    | "list" -> Obj.magic (to_list convert elt : 'a list)
-    | "option" -> Obj.magic (to_option convert elt : 'a option)
-    | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b))
-    | "goals" -> Obj.magic (to_goals elt : goals)
-    | "evar" -> Obj.magic (to_evar elt : evar)
-    | "option_value" -> Obj.magic (to_option_value elt : option_value)
-    | "option_state" -> Obj.magic (to_option_state elt : option_state)
-    | _ -> raise Marshal_error
-    end
-  | _ -> raise Marshal_error
-  in
-  to_value convert xml
-
-(** * Debug printing *)
-
-let pr_option_value = function
-| IntValue None -> "none"
-| IntValue (Some i) -> string_of_int i
-| StringValue s -> s
-| BoolValue b -> if b then "true" else "false"
-
-let rec pr_setoptions opts =
-  let map (key, v) =
-    let key = String.concat " " key in
-    key ^ " := " ^ (pr_option_value v)
-  in
-  String.concat "; " (List.map map opts)
-
-let pr_getoptions opts =
-  let map (key, s) =
-    let key = String.concat " " key in
-    Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n"
-      key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
-  in
-  "\n" ^ String.concat "" (List.map map opts)
-
-let pr_call = function
-  | Interp (r,b,s) ->
-    let raw = if r then "RAW" else "" in
-    let verb = if b then "" else "SILENT" in
-    "INTERP"^raw^verb^" ["^s^"]"
-  | Rewind i -> "REWIND "^(string_of_int i)
-  | Goal -> "GOALS"
-  | Evars -> "EVARS"
-  | Hints -> "HINTS"
-  | Status -> "STATUS"
-  | GetOptions -> "GETOPTIONS"
-  | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
-  | InLoadPath s -> "INLOADPATH "^s
-  | MkCases s -> "MKCASES "^s
-
-let pr_value_gen pr = function
-  | Good v -> "GOOD " ^ pr v
-  | Fail (_,str) -> "FAIL ["^str^"]"
-
-let pr_value v = pr_value_gen (fun _ -> "") v
-
-let pr_string s = "["^s^"]"
-let pr_bool b = if b then "true" else "false"
-
-let pr_status s =
-  let path =
-    let l = String.concat "." s.status_path in
-    "path=" ^ l ^ ";"
-  in
-  let name = match s.status_proofname with
-  | None -> "no proof;"
-  | Some n -> "proof = " ^ n ^ ";"
-  in
-  "Status: " ^ path ^ name
-
-let pr_mkcases l =
-  let l = List.map (String.concat " ") l in
-  "[" ^ String.concat " | " l ^ "]"
-
-let pr_goals_aux g =
-  if g.fg_goals = [] then
-    if g.bg_goals = [] then "Proof completed."
-    else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals)
-  else
-    let pr_menu s = s in
-    let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-      "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]"
-    in
-    String.concat " " (List.map pr_goal g.fg_goals)
-
-let pr_goals = function
-| None -> "No proof in progress."
-| Some g -> pr_goals_aux g
-
-let pr_evar ev = "[" ^ ev.evar_info ^ "]"
-
-let pr_evars = function
-| None -> "No proof in progress."
-| Some evars -> String.concat " " (List.map pr_evar evars)
-
-let pr_full_value call value =
-  match call with
-    | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
-    | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
-    | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value)
-    | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value)
-    | Hints -> pr_value value
-    | Status -> pr_value_gen pr_status (Obj.magic value : status value)
-    | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value)
-    | SetOptions _ -> pr_value value
-    | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
-    | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
deleted file mode 100644
index 69204da167..0000000000
--- a/toplevel/ide_intf.mli
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** * Applicative part of the interface of CoqIde calls to Coq *)
-
-open Interface
-
-type xml = Xml_parser.xml
-
-type 'a call
-
-(** Running a command (given as a string).
-    - The 1st flag indicates whether to use "raw" mode
-      (less sanity checks, no impact on the undo stack).
-      Suitable e.g. for queries, or for the Set/Unset
-      of display options that coqide performs all the time.
-    - The 2nd flag controls the verbosity.
-    - The returned string contains the messages produced
-      by this command, but not the updated goals (they are
-      to be fetch by a separated [current_goals]). *)
-val interp : raw * verbose * string -> string call
-
-(** Backtracking by at least a certain number of phrases.
-    No finished proofs will be re-opened. Instead,
-    we continue backtracking until before these proofs,
-    and answer the amount of extra backtracking performed.
-    Backtracking by more than the number of phrases already
-    interpreted successfully (and not yet undone) will fail. *)
-val rewind : int -> int call
-
-(** Fetching the list of current goals. Return [None] if no proof is in 
-    progress, [Some gl] otherwise. *)
-val goals : goals option call
-
-(** Retrieving the tactics applicable to the current goal. [None] if there is 
-    no proof in progress. *)
-val hints : (hint list * hint) option call
-
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val status : status call
-
-(** Is a directory part of Coq's loadpath ? *)
-val inloadpath : string -> bool call
-
-(** Create a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables. *)
-val mkcases : string -> string list list call
-
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
-    proof is in progress. *)
-val evars : evar list option call
-
-(** Retrieve the list of options of the current toplevel, together with their 
-    state. *)
-val get_options : (option_name * option_state) list call
-
-(** Set the options to the given value. Warning: this is not atomic, so whenever
-    the call fails, the option state can be messed up... This is the caller duty
-    to check that everything is correct. *)
-val set_options : (option_name * option_value) list -> unit call
-
-val abstract_eval_call : handler -> 'a call -> 'a value
-
-(** * XML data marshalling *)
-
-exception Marshal_error
-
-val of_value : ('a -> xml) -> 'a value -> xml
-val to_value : (xml -> 'a) -> xml -> 'a value
-
-val of_call : 'a call -> xml
-val to_call : xml -> 'a call
-
-val of_answer : 'a call -> 'a value -> xml
-val to_answer : xml -> 'a value
-
-(** * Debug printing *)
-
-val pr_call : 'a call -> string
-val pr_value : 'a value -> string
-val pr_full_value : 'a call -> 'a value -> string
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index f8bf9fccbd..41a5f48a66 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -219,7 +219,7 @@ let hints () =
 (** Other API calls *)
 
 let inloadpath dir =
-  Library.is_in_load_paths (System.physical_path_of_string dir)
+  Library.is_in_load_paths (CUnix.physical_path_of_string dir)
 
 let status () =
   (** We remove the initial part of the current [dir_path]
@@ -295,7 +295,7 @@ let eval_call c =
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());
-  Ide_intf.abstract_eval_call handler c
+  Serialize.abstract_eval_call handler c
 
 
 (** The main loop *)
@@ -311,7 +311,7 @@ let pr_debug s =
   if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let fail err =
-  Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err))
+  Serialize.of_value (fun _ -> assert false) (Interface.Fail (None, err))
 
 let loop () =
   let p = Xml_parser.make () in
@@ -326,16 +326,16 @@ let loop () =
       let xml_answer =
         try
           let xml_query = Xml_parser.parse p (Xml_parser.SChannel stdin) in
-          let q = Ide_intf.to_call xml_query in
-          let () = pr_debug ("<-- " ^ Ide_intf.pr_call q) in
+          let q = Serialize.to_call xml_query in
+          let () = pr_debug ("<-- " ^ Serialize.pr_call q) in
           let r = eval_call q in
-          let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in
-          Ide_intf.of_answer q r
+          let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in
+          Serialize.of_answer q r
         with
         | Xml_parser.Error (err, loc) ->
           let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in
           fail msg
-        | Ide_intf.Marshal_error ->
+        | Serialize.Marshal_error ->
           fail "Incorrect query."
       in
       Xml_utils.print_xml !orig_stdout xml_answer;
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
deleted file mode 100644
index 6040605504..0000000000
--- a/toplevel/interface.mli
+++ /dev/null
@@ -1,93 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** * Declarative part of the interface of CoqIde calls to Coq *)
-
-(** * Generic structures *)
-
-type raw = bool
-type verbose = bool
-
-(** The type of coqtop goals *)
-type goal = {
-  goal_hyp : string list;
-  (** List of hypotheses *)
-  goal_ccl : string;
-  (** Goal conclusion *)
-}
-
-type evar = {
-  evar_info : string;
-  (** A string describing an evar: type, number, environment *)
-}
-
-type status = {
-  status_path : string list;
-  (** Module path of the current proof *)
-  status_proofname : string option;
-  (** Current proof name. [None] if no focussed proof is in progress *)
-  status_allproofs : string list;
-  (** List of all pending proofs. Order is not significant *)
-  status_statenum : int;
-  (** A unique id describing the state of coqtop *)
-  status_proofnum : int;
-  (** An id describing the state of the current proof. *)
-}
-
-type goals = {
-  fg_goals : goal list;
-  (** List of the focussed goals *)
-  bg_goals : goal list;
-  (** List of the background goals *)
-}
-
-type hint = (string * string) list
-(** A list of tactics applicable and their appearance *)
-
-type option_name = Goptionstyp.option_name
-
-type option_value = Goptionstyp.option_value =
-  | BoolValue   of bool
-  | IntValue    of int option
-  | StringValue of string
-
-(** Summary of an option status *)
-type option_state = Goptionstyp.option_state = {
-  opt_sync  : bool;
-  (** Whether an option is synchronous *)
-  opt_depr  : bool;
-  (** Wheter an option is deprecated *)
-  opt_name  : string;
-  (** A short string that is displayed when using [Test] *)
-  opt_value : option_value;
-  (** The current value of the option *)
-}
-
-(** * Coq answers to CoqIde *)
-
-type location = (int * int) option (* start and end of the error *)
-
-type 'a value =
-  | Good of 'a
-  | Fail of (location * string)
-
-(** * The structure that coqtop should implement *)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals option;
-  evars : unit -> evar list option;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  get_options : unit -> (option_name * option_state) list;
-  set_options : (option_name * option_value) list -> unit;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  handle_exn : exn -> location * string;
-}
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index da9575ca6e..e02e6329da 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -10,7 +10,7 @@ open Errors
 open Util
 open Pp
 open Flags
-open System
+open CUnix
 open Libobject
 open Library
 open System
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 599f8e9ffb..b46d8fa8a3 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -21,7 +21,6 @@ Vernacentries
 G_obligations
 Whelp
 Vernac
-Ide_intf
 Ide_slave
 Toplevel
 Usage
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8c9b10786b..b4add69ae5 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -90,7 +90,7 @@ let print_usage_coqc () =
 
 let print_config () =
   if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
-  Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
+  Printf.printf "COQLIB=%s/\n" (Envars.coqlib Errors.error);
   Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
   Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
   Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 20b45a2b08..916d213f58 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -172,7 +172,7 @@ let pr_new_syntax loc ocom =
 let rec vernac_com interpfun checknav (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
-	let fname = expand_path_macros fname in
+	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
         (* translator state *)
         let ch = !chan_beautify in
         let cs = Lexer.com_state() in
@@ -184,13 +184,13 @@ let rec vernac_com interpfun checknav (loc,com) =
 	    begin
               let _,f = find_file_in_path ~warn:(Flags.is_verbose())
 		(Library.get_load_paths ())
-		(make_suffix fname ".v") in
+		(CUnix.make_suffix fname ".v") in
 		chan_beautify := open_out (f^beautify_suffix);
 		Pp.comments := []
             end;
           begin
 	    try
-	      read_vernac_file verbosely (make_suffix fname ".v");
+	      read_vernac_file verbosely (CUnix.make_suffix fname ".v");
               if !Flags.beautify_file then close_out !chan_beautify;
               chan_beautify := ch;
               Lexer.restore_com_state cs;
@@ -228,7 +228,7 @@ let rec vernac_com interpfun checknav (loc,com) =
     | VernacTime v ->
 	  let tstart = System.get_time() in
           interp v;
-	  let tend = System.get_time() in
+	  let tend = get_time() in
           msgnl (str"Finished transaction in " ++
                    System.fmt_time_difference tstart tend)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 355e693569..538a502ec0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -708,33 +708,35 @@ let vernac_set_used_variables l =
 
 let vernac_require_from export filename =
   Library.require_library_from_file None
-    (System.expand_path_macros filename)
+    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename)
     export
 
 let vernac_add_loadpath isrec pdir ldiropt =
-  let pdir = System.expand_path_macros pdir in
+  let pdir = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) pdir in
   let alias = match ldiropt with
     | None -> Nameops.default_root_prefix
     | Some ldir -> ldir in
   (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias
 
 let vernac_remove_loadpath path =
-  Library.remove_load_path (System.expand_path_macros path)
+  Library.remove_load_path (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
 
   (* Coq syntax for ML or system commands *)
 
 let vernac_add_ml_path isrec path =
   (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
-    (System.expand_path_macros path)
+    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
 
 let vernac_declare_ml_module local l =
-  Mltop.declare_ml_modules local (List.map System.expand_path_macros l)
+  Mltop.declare_ml_modules local (List.map
+				    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)))
+				    l)
 
 let vernac_chdir = function
   | None -> message (Sys.getcwd())
   | Some path ->
       begin
-	try Sys.chdir (System.expand_path_macros path)
+	try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
 	with Sys_error str -> warning ("Cd failed: " ^ str)
       end;
       if_verbose message (Sys.getcwd())
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e9ecc95ecb..c8729bfa97 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -134,7 +134,7 @@ type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 type full_locality_flag = bool option (* true = Local; false = Global      *)
 
-type option_value = Goptionstyp.option_value =
+type option_value = Interface.option_value =
   | BoolValue of bool
   | IntValue of int option
   | StringValue of string
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 332d30536c..5da85be03f 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -177,7 +177,7 @@ let make_string f x = Buffer.reset b; f x; Buffer.contents b
 let send_whelp req s =
   let url = make_whelp_request req s in
   let command = subst_command_placeholder browser_cmd_fmt url in
-  let _ = run_command (fun x -> x) print_string command in ()
+  let _ = CUnix.run_command (fun x -> x) print_string command in ()
 
 let whelp_constr req c =
   let c = detype false [whelm_special] [] c in