5 files changed, 50 insertions, 28 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index fda25a0a60..0cf989e494 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -120,7 +120,7 @@ let uniquize_flags_rev flags =
 
 (** [normalize_flags] removes redundant warnings. Unknown warnings are kept
     because they may be declared in a plugin that will be linked later. *)
-let normalize_flags ~silent warnings =
+let normalize_flags warnings =
   let warnings = cut_before_all_rev warnings in
   uniquize_flags_rev warnings
 
@@ -130,7 +130,7 @@ let normalize_flags_string s =
   if is_none_keyword s then s
   else
     let flags = flags_of_string s in
-    let flags = normalize_flags ~silent:false flags in
+    let flags = normalize_flags flags in
     string_of_flags flags
 
 let parse_warnings items =
@@ -146,7 +146,7 @@ let parse_flags s =
   else begin
       Flags.make_warn true;
       let flags = flags_of_string s in
-      let flags = normalize_flags ~silent:true flags in
+      let flags = normalize_flags flags in
       parse_warnings flags;
       string_of_flags flags
     end
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml
index 61eb1dafdf..c2bcd73fff 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml
@@ -90,30 +90,50 @@ let rec post_canonize f =
 
 exception Parsing_error of string
 
-let rec parse_string = parser
-  | [< '' ' | '\n' | '\t' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
-  | [< >] -> ""
-and parse_string2 = parser
-  | [< ''"' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
-  | [< >] -> raise (Parsing_error "unterminated string")
-and parse_skip_comment = parser
-  | [< ''\n'; s >] -> s
-  | [< 'c; s >] -> parse_skip_comment s
-  | [< >] -> [< >]
-and parse_args = parser
-  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
-  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
-  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
-  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
-  | [< >] -> []
+let buffer buf =
+  let ans = Buffer.contents buf in
+  let () = Buffer.clear buf in
+  ans
+
+let rec parse_string buf s = match Stream.next s with
+| ' ' | '\n' | '\t' -> buffer buf
+| c ->
+  let () = Buffer.add_char buf c in
+  parse_string buf s
+| exception Stream.Failure -> buffer buf
+
+and parse_string2 buf s = match Stream.next s with
+| '"' -> buffer buf
+| c ->
+  let () = Buffer.add_char buf c in
+  parse_string2 buf s
+| exception Stream.Failure -> raise (Parsing_error "unterminated string")
+
+and parse_skip_comment s = match Stream.next s with
+| '\n' -> ()
+| _ -> parse_skip_comment s
+| exception Stream.Failure -> ()
+
+and parse_args buf accu s = match Stream.next s with
+| ' ' | '\n' | '\t' -> parse_args buf accu s
+| '#' ->
+  let () = parse_skip_comment s in
+  parse_args buf accu s
+| '"' ->
+  let str = parse_string2 buf s in
+  parse_args buf (str :: accu) s
+| c ->
+  let () = Buffer.add_char buf c in
+  let str = parse_string buf s in
+  parse_args buf (str :: accu) s
+| exception Stream.Failure -> accu
 
 let parse f =
   let c = open_in f in
-  let res = parse_args (Stream.of_channel c) in
+  let buf = Buffer.create 64 in
+  let res = parse_args buf [] (Stream.of_channel c) in
   close_in c;
-  res
+  List.rev res
 ;;
 
 (* Copy from minisys.ml, since we don't see that file here *)
@@ -143,7 +163,7 @@ let process_cmd_line orig_dir proj args =
     error "Use \"-install none\" instead of \"-no-install\""
   | "-custom" :: _ ->
     error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
-  
+
   | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt =  false } r
   | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
   | "-install" :: d :: r ->
@@ -189,7 +209,7 @@ let process_cmd_line orig_dir proj args =
       error "Output file must be in the current directory";
     if proj.makefile <> None then
       error "Option -o given more than once";
-    aux { proj with makefile = Some file } r  
+    aux { proj with makefile = Some file } r
   | v :: "=" :: def :: r ->
     aux { proj with defs = proj.defs @ [sourced (v,def)] } r
   | "-arg" :: a :: r ->
diff --git a/lib/envars.ml b/lib/envars.ml
index be82bfe9bb..3ee0c7106b 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -110,6 +110,7 @@ let check_file_else ~dir ~file oth =
   if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
+  getenv_else "COQLIB" (fun () ->
   let prelude = "theories/Init/Prelude.vo" in
   check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
     (fun () ->
@@ -117,6 +118,7 @@ let guess_coqlib fail =
       then Coq_config.coqlib
       else
         fail "cannot guess a path for Coq libraries; please use -coqlib option")
+  )
 
 (** coqlib is now computed once during coqtop initialization *)
 
diff --git a/lib/system.ml b/lib/system.ml
index f109c71925..eef65a4e3d 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -302,7 +302,7 @@ let with_time ~batch f x =
     raise e
 
 let get_toplevel_path top =
-  let dir = Filename.dirname Sys.argv.(0) in
+  let dir = Filename.dirname Sys.executable_name in
   let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
   let eff = if Dynlink.is_native then ".opt" else ".byte" in
   dir ^ Filename.dir_sep ^ top ^ eff ^ exe
diff --git a/lib/util.ml b/lib/util.ml
index 7d7d380b26..38d73d3453 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -38,8 +38,8 @@ let is_blank = function
 
 module Empty =
 struct
-  type t
-  let abort (x : t) = assert false
+  type t = { abort : 'a. 'a }
+  let abort (x : t) = x.abort
 end
 
 (* Strings *)