Made the debugger work again:

- call to open_process_full from Envars.camlp4lib was apparently
  disturbing stdin/stdout/stderr and precipitating coqtop.byte death
  in ocamldebug; renounced to add camlp4 to the ml path (why was it useful?)
  which was the reason for calling camlp4lib (seems like camlp4lib
  is now useless),
- Envars was needing str.cma which was missing when calling printers.cma;
  renounced to use str.cma since its only use was for an elementary 
  split function.


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

4 files changed, 14 insertions, 12 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 82e0d3162..e67fc32d9 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -30,8 +30,8 @@ let coqlib () =
     (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
 
 let path_to_list p =
-  let sep = Str.regexp_string (if Sys.os_type = "Win32" then ";" else ":") in
-    Str.split sep p 
+  let sep = if Sys.os_type = "Win32" then ';' else ':' in
+    Util.split_string_at sep p 
 
 let rec which l f =
   match l with
diff --git a/lib/util.ml b/lib/util.ml
index 6803412fd..fe715f0a7 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -109,19 +109,23 @@ let ordinal n =
 
 (* string parsing *)
 
-let parse_loadpath s =
+let split_string_at c s =
   let len = String.length s in
-  let rec decoupe_dirs n =
+  let rec split n =
     try  
-      let pos = String.index_from s n '/' in
-      if pos = n then
-	invalid_arg "parse_loadpath: find an empty dir in loadpath";
+      let pos = String.index_from s n c in
       let dir = String.sub s n (pos-n) in
-      dir :: (decoupe_dirs (succ pos))
+      dir :: split (succ pos)
     with
       | Not_found -> [String.sub s n (len-n)]
   in
-  if len = 0 then [] else decoupe_dirs 0
+  if len = 0 then [] else split 0
+
+let parse_loadpath s =
+  let l = split_string_at '/' s in
+  if List.mem "" l then
+    invalid_arg "parse_loadpath: find an empty dir in loadpath";
+  l
 
 module Stringset = Set.Make(struct type t = string let compare = compare end)
 
diff --git a/lib/util.mli b/lib/util.mli
index 49e1fb4bd..b6403fd73 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -77,6 +77,7 @@ val string_index_from : string -> int -> string -> int
 val string_string_contains : where:string -> what:string -> bool
 val plural : int -> string -> string
 val ordinal : int -> string
+val split_string_at : char -> string -> string list
 
 val parse_loadpath : string -> string list
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index a21e33c87..90a36620a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -98,7 +98,6 @@ let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let dirs = "states" :: ["contrib"] in
-  let camlp4 = Envars.camlp4lib () in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then 
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
@@ -110,8 +109,6 @@ let init_load_path () =
     List.iter 
       (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) 
       theories_dirs_map;
-    (* then camlp4lib *)
-    add_ml_include camlp4;
     (* then current directory *)
     Mltop.add_path "." Nameops.default_root_prefix;
     (* additional loadpath, given with -I -include -R options *)