Misc changes around coqtop.ml :

 - Revised Coqtop.parse_args in a cleaner and lighter style
 - Improved error message in case of argument parse failure:
   * tell which option is expecting a related argument
   * in case of unknown options, warn about them all at once
   * do not hide the previous error messages by filling the
     screen with usage(). Instead, suggest the use of --help.
 - Specialized boolean config field Coq_config.arch_is_win32
 - Faster Envars.coqlib, which is back to (unit->string), and
   just access Flags.coqlib. Caveat: it must be initialized once
   via Envars.set_coqlib
 - Avoid keeping an opened channel to the "revision" file
 - Direct load of theories/init/prelude.vo, no detour via Loadpath

Beware : ./configure must be runned after this commit

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

21 files changed, 247 insertions, 263 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 280f34656..d54e9328a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -42,21 +42,21 @@ let path_of_string s =
       [] -> invalid_arg "path_of_string"
     | l::dir -> {dirpath=dir; basename=l}
 
-let (/) = Filename.concat
+let ( / ) = Filename.concat
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib error in
-    let ch = open_in (Filename.concat coqlib "revision") in
+    let ch = open_in (Envars.coqlib () / "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
-      (ver,rev)
+    let () = close_in ch in
+    (ver,rev)
   with _ -> (Coq_config.version,Coq_config.date)
 
 let print_header () =
   let (ver,rev) = (get_version_date ()) in
-    Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
-    flush stdout
+  Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
+  flush stdout
 
 (* Adding files to Coq loadpath *)
 
@@ -107,7 +107,7 @@ let set_rec_include d p =
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib error in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs in
   let coqpath = Envars.coqpath in
@@ -306,7 +306,9 @@ let parse_args argv =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (Envars.coqlib error); exit 0
+        Envars.set_coqlib ~fail:Errors.error;
+        print_endline (Envars.coqlib ());
+        exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
@@ -341,6 +343,7 @@ let init_with_argv argv =
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     try
       parse_args argv;
+      Envars.set_coqlib ~fail:Errors.error;
       if_verbose print_header ();
       init_load_path ();
       engage ();
diff --git a/config/coq_config.mli b/config/coq_config.mli
index f16ffbe51..94d0b6c93 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -36,6 +36,7 @@ val cflags : string     (* arguments passed to gcc *)
 
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
+val arch_is_win32 : bool
 val osdeplibs : string  (* OS dependant link options for ocamlc *)
 val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
 
diff --git a/configure b/configure
index 43317f1f5..1cfb4f125 100755
--- a/configure
+++ b/configure
@@ -311,10 +311,12 @@ esac
 # executable extension
 
 case $ARCH in
-    win32) 
+    win32)
+      ARCH_WIN32=true
       EXE=".exe"
       DLLEXT=".dll";;
-    *) EXE=""
+    *) ARCH_WIN32=false
+       EXE=""
        DLLEXT=".so"
 esac
 
@@ -1042,6 +1044,7 @@ let coqideincl = "$LABLGTKINCLUDES"
 let cflags = "$cflags"
 let best = "$best_compiler"
 let arch = "$ARCH"
+let arch_is_win32 = $ARCH_WIN32
 let has_coqide = "$COQIDE"
 let gtk_platform = \`$IDEARCHDEF
 let has_natdynlink = $HASNATDYNLINK
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 2256764a3..aac7f9a28 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -117,6 +117,9 @@ let init_modules = [
   init_dir@["Wf"]
 ]
 
+let prelude_module_name = init_dir@["Prelude"]
+let prelude_module = make_dir prelude_module_name
+
 let logic_module_name = init_dir@["Logic"]
 let logic_module = make_dir logic_module_name
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index b8e461665..9e0cfadae 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -54,6 +54,8 @@ val check_required_library : string list -> unit
 (** {6 Global references } *)
 
 (** Modules *)
+val prelude_module : DirPath.t
+
 val logic_module : DirPath.t
 val logic_module_name : string list
 
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 74c60f75b..1a44fac6c 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -30,11 +30,13 @@ let dump () = !glob_output != NoGlob
 
 let noglob () = glob_output := NoGlob
 
-let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
-
 let dump_to_dotglob () = glob_output := MultFiles
 
-let dump_into_file f = glob_output := File f; open_glob_file f
+let dump_into_file f =
+  if String.equal f "stdout" then
+    (glob_output := StdOut; glob_file := Pervasives.stdout)
+  else
+    (glob_output := File f; open_glob_file f)
 
 let dump_string s =
   if dump () then Pervasives.output_string !glob_file s
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index edea94f0c..37370f6e1 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -15,8 +15,7 @@ val end_dump_glob : unit -> unit
 val dump : unit -> bool
 
 val noglob : unit -> unit
-val dump_to_stdout : unit -> unit
-val dump_into_file : string -> unit
+val dump_into_file : string -> unit (** special handling of "stdout" *)
 val dump_to_dotglob : unit -> unit
 
 val pause : unit -> unit
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 6b2b4aa7c..c9da5222f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -32,13 +32,12 @@ let open_header = List.map mk_open open_header
 let compiler_name =
   Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ())
 
-let ( / ) a b = Filename.concat a b
+let ( / ) = Filename.concat
 
 (* We have to delay evaluation of include_dirs because coqlib cannot be guessed
 until flags have been properly initialized *)
-let include_dirs () = [Filename.temp_dir_name;
-                    coqlib ~fail:Errors.error / "kernel";
-                    coqlib ~fail:Errors.error / "library"]
+let include_dirs () =
+  [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"]
 
 (* Pointer to the function linking an ML object into coq's toplevel *)
 let load_obj = ref (fun x -> () : string -> unit)
diff --git a/lib/envars.ml b/lib/envars.ml
index cf3d6503d..5e20df358 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -87,53 +87,48 @@ let coqbin =
 
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)
-let coqroot = 
+let coqroot =
   Filename.dirname coqbin
-    
+
 (** On win32, we add coqbin to the PATH at launch-time (this used to be
     done in a .bat script). *)
 let _ =
-  if String.equal Coq_config.arch "win32" then
+  if Coq_config.arch_is_win32 then
     Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
 
-(** [reldir instdir testfile oth] checks if [testfile] exists in 
-    the installation directory [instdir] given relatively to 
-    [coqroot]. If this Coq is only locally built, then [testfile]
-    must be found at [coqroot]. 
+(** [check_file_else ~dir ~file oth] checks if [file] exists in
+    the installation directory [dir] given relatively to [coqroot].
+    If this Coq is only locally built, then [file] must be in [coqroot].
     If the check fails, then [oth ()] is evaluated. *)
-let reldir instdir testfile oth =
-  let rpath = if Coq_config.local then [] else instdir in
-  let out = List.fold_left ( / ) coqroot rpath in
-  if Sys.file_exists (out / testfile) then out else oth ()
+let check_file_else ~dir ~file oth =
+  let path = if Coq_config.local then coqroot else coqroot / dir in
+  if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
-  let file = "theories/Init/Prelude.vo" in
-    reldir (if String.equal Coq_config.arch "win32" then ["lib"] else ["lib";"coq"]) file
-      (fun () ->
-        let coqlib = match Coq_config.coqlib with
-          | Some coqlib -> coqlib
-          | None -> coqroot
-        in
-        if Sys.file_exists (coqlib / file) then 
-	  coqlib
-        else 
-	  fail "cannot guess a path for Coq libraries; please use -coqlib option")
-
-let coqlib ~fail =
-  if !Flags.coqlib_spec then 
-    !Flags.coqlib 
-  else if !Flags.boot then 
-    coqroot 
-  else 
-    guess_coqlib fail
+  let prelude = "theories/Init/Prelude.vo" in
+  let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in
+  check_file_else ~dir ~file:prelude
+    (fun () ->
+      let coqlib = match Coq_config.coqlib with
+        | Some coqlib -> coqlib
+        | None -> coqroot
+      in
+      if Sys.file_exists (coqlib / prelude) then coqlib
+      else
+        fail "cannot guess a path for Coq libraries; please use -coqlib option")
+
+(** coqlib is now computed once during coqtop initialization *)
+
+let set_coqlib ~fail =
+  if not !Flags.coqlib_spec then
+    let lib = if !Flags.boot then coqroot else guess_coqlib fail in
+    Flags.coqlib := lib
+
+let coqlib () = !Flags.coqlib
 
 let docdir () =
-  reldir (
-    if String.equal Coq_config.arch "win32" then 
-      ["doc"] 
-    else 
-      ["share";"doc";"coq"]
-  ) "html" (fun () -> Coq_config.docdir)
+  let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in
+  check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir)
 
 let coqpath =
   let coqpath = getenv_else "COQPATH" (fun () -> "") in
diff --git a/lib/envars.mli b/lib/envars.mli
index c0142a8d7..19ba8d2c0 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -25,7 +25,10 @@ val expand_path_macros : warn:(string -> unit) -> string -> string
 val home : warn:(string -> unit) -> string
 
 (** [coqlib] is the path to the Coq library. *)
-val coqlib : fail:(string -> string) -> string
+val coqlib : unit -> string
+
+(** [set_coqlib] must be runned once before any access to [coqlib] *)
+val set_coqlib : fail:(string -> string) -> unit
 
 (** [docdir] is the path to the Coq documentation. *)
 val docdir : unit -> string
diff --git a/lib/flags.ml b/lib/flags.ml
index 43ebe1491..9f4e81408 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -168,11 +168,7 @@ let canonical_path_name p =
 
 (* Options for changing coqlib *)
 let coqlib_spec = ref false
-let coqlib = ref (
-  (* same as Envars.coqroot, but copied here because of dependencies *)
-  Filename.dirname
-    (canonical_path_name (Filename.dirname Sys.executable_name))
-)
+let coqlib = ref "(not initialized yet)"
 
 (* Options for changing camlbin (used by coqmktop) *)
 let camlbin_spec = ref false
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index a0e2e7ef7..5a03470a4 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -58,7 +58,7 @@ let _ = begin
   Options.ocamllex := A Coq_config.ocamllex;
 end
 
-let w32 = (Coq_config.arch = "win32")
+let w32 = Coq_config.arch_is_win32
 
 let w32pref = "i586-mingw32msvc"
 let w32ocamlc = w32pref^"-ocamlc"
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eff1d4ba9..082814655 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1764,7 +1764,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste
   Lazy.force require_csdp;
 
   let cmdname =
-    List.fold_left Filename.concat (Envars.coqlib ~fail:Errors.error)
+    List.fold_left Filename.concat (Envars.coqlib ())
       ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
 
     match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 6afba15bf..11e558a76 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -11,7 +11,6 @@ open Nametab
 open Term
 open Globnames
 open Libobject
-open Library
 
 (** Operations concerning records and canonical structures *)
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index e15a1768c..2d9c2fd33 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -117,9 +117,14 @@ let parse_args () =
     | ("-v"|"--version") :: _ -> Usage.version 0
 
     | ("-where") :: _ ->
-	print_endline (Envars.coqlib (fun x -> x)); exit 0
+        Envars.set_coqlib (fun x -> x);
+        print_endline (Envars.coqlib ());
+        exit 0
 
-    | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
+    | ("-config" | "--config") :: _ ->
+        Envars.set_coqlib (fun x -> x);
+        Usage.print_config ();
+        exit 0
 
 (* Options for coqtop : a) options with 0 argument *)
 
@@ -132,7 +137,7 @@ let parse_args () =
       |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
 	parse (cfiles,o::args) rem
 
-(* Options for coqtop : a) options with 1 argument *)
+(* Options for coqtop : b) options with 1 argument *)
 
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
@@ -144,7 +149,7 @@ let parse_args () =
 	    | []        -> usage ()
 	end
 
-(* Options for coqtop : a) options with 1 argument and possibly more *)
+(* Options for coqtop : c) options with 1 argument and possibly more *)
 
     | ("-I"|"-include" as o) :: rem ->
 	begin
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f296594d1..16e5bbde8 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -198,7 +198,8 @@ let coqdep () =
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"]
   end else begin
-    let coqlib = Envars.coqlib Errors.error in
+    Envars.set_coqlib ~fail:Errors.error;
+    let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 070778fb2..b356ac537 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let ( / ) = Filename.concat
+
 let coqdoc_out f =
   if !output_dir <> "" && Filename.is_relative f then
     if not (Sys.file_exists !output_dir) then
       (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
     else
-      Filename.concat !output_dir f
+      !output_dir / f
   else
     f
 
@@ -73,15 +75,17 @@ let normalize_filename f =
 let guess_coqlib () =
   let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
-      coqlib
+    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
     | Some _ | None ->
       let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      let rpath =
+        if Coq_config.local then []
+        else if Coq_config.arch_is_win32 then ["lib"]
+        else ["lib/coq"]
+      in
+      let coqlib = List.fold_left (/) prefix rpath in
+      if Sys.file_exists (coqlib / file) then coqlib
       else prefix
 
 let header_trailer = ref true
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 39a8ede9a..0ab732da2 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -72,10 +72,10 @@ let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
    below (for accessing the corresponding .cmi). *)
 
 let src_dirs =
-  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]  ]
+  [ []; ["lib"]; ["toplevel"]; ["kernel/byterun"]  ]
 
 let includes () =
-  let coqlib = if !Flags.boot then "." else Envars.coqlib ~fail:Errors.error in
+  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
   let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
   (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
   @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
@@ -259,6 +259,7 @@ let create_tmp_main_file modules =
 (* main part *)
 let main () =
   let (options, userfiles) = parse_args () in
+  let () = Envars.set_coqlib ~fail:Errors.error in
   (* which ocaml command to invoke *)
   let camlbin = Envars.camlbin () in
   let prog =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index dfe576a69..3841f4f9c 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -9,7 +9,7 @@
 open Util
 open Pp
 
-let (/) = Filename.concat
+let ( / ) = Filename.concat
 
 let set_debug () =
   let () = Backtrace.record_backtrace true in
@@ -97,7 +97,7 @@ let theories_dirs_map = [
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib ~fail:Errors.error in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
@@ -135,7 +135,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 ~fail:Errors.error);
+    Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c0b47f0c1..79467cacd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -18,22 +18,24 @@ open Coqinit
 
 let () = at_exit flush_all
 
+let ( / ) = Filename.concat
+
 let fatal_error info =
   pperrnl info; flush_all (); exit 1
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib ~fail:Errors.error in
-    let ch = open_in (Filename.concat coqlib "revision") in
+    let ch = open_in (Envars.coqlib () / "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
-      (ver,rev)
+    let () = close_in ch in
+    (ver,rev)
   with e when Errors.noncritical e ->
     (Coq_config.version,Coq_config.date)
 
 let print_header () =
-  let (ver,rev) = (get_version_date ()) in
-  pp (str "Welcome to Coq "++ str ver ++ str " (" ++ str rev ++ str ")" ++ fnl ());
+  let (ver,rev) = get_version_date () in
+  ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
   pp_flush ()
 
 let output_context = ref false
@@ -42,7 +44,8 @@ let memory_stat = ref false
 
 let print_memory_stat () =
   if !memory_stat then
-    pp (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ())
+    ppnl
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
 
 let _ = at_exit print_memory_stat
 
@@ -99,8 +102,8 @@ let load_vernac_obj () =
 let load_init = ref true
 
 let require_prelude () =
-  let q = qualid_of_string "Coq.Init.Prelude" in
-  Library.require_library [Loc.ghost,q] (Some true)
+  let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
+  Library.require_library_from_dirpath [Coqlib.prelude_module,vo] (Some true)
 
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
@@ -111,10 +114,12 @@ let require () =
 
 let compile_list = ref ([] : (bool * string) list)
 
-let add_compile verbose glob_opt s =
+let glob_opt = ref false
+
+let add_compile verbose s =
   set_batch_mode ();
   Flags.make_silent true;
-  if not glob_opt then Dumpglob.dump_to_dotglob ();
+  if not !glob_opt then Dumpglob.dump_to_dotglob ();
   compile_list := (verbose,s) :: !compile_list
 
 let compile_file (v,f) =
@@ -146,6 +151,14 @@ let set_vm_opt () =
   Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
+(** Options for proof general *)
+
+let set_emacs () =
+  Flags.print_emacs := true;
+  Pp.make_pp_emacs ();
+  Vernacentries.qed_display_script := false;
+  Flags.make_term_color false
+
 (** GC tweaking *)
 
 (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
@@ -182,186 +195,134 @@ let usage () =
   flush stderr ;
   exit 1
 
+let error_missing_arg s =
+  prerr_endline ("Error: extra argument expected after option "^s);
+  prerr_endline "See --help for the syntax of supported options";
+  exit 1
+
 let warning s = msg_warning (strbrk s)
 
 let filter_opts = ref false
+let exitcode () = if !filter_opts then 2 else 0
 
 let verb_compat_ntn = ref false
 let no_compat_ntn = ref false
 
-let parse_args arglist =
-  let glob_opt = ref false in
-  let rec parse = function
-    | [] -> []
-    | "-with-geoproof" :: s :: rem ->
-	if String.equal s "yes" then Coq_config.with_geoproof := true
-	else if String.equal s "no" then Coq_config.with_geoproof := false
-	else usage ();
-	parse rem
-    | "-impredicative-set" :: rem ->
-        set_engagement Declarations.ImpredicativeSet; parse rem
-
-    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
-    | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
-    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
-    | ("-I"|"-include") :: []       -> usage ()
-
-    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: d :: "-as" :: [] -> usage ()
-    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: ([] | [_]) -> usage ()
-
-    | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
-    | "-top" :: [] -> usage ()
-
-    | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
-    | "-exclude-dir" :: [] -> usage ()
-
-    | "-notop" :: rem -> unset_toplevel_name (); parse rem
-    | "-q" :: rem -> no_load_rc (); parse rem
-
-    | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem
-    | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem
-    | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
-
-    | "-batch" :: rem -> set_batch_mode (); parse rem
-    | "-boot" :: rem -> boot := true; no_load_rc (); parse rem
-    | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
-    | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
-    | "-outputstate" :: []       -> usage ()
-
-    | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem
-
-    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
-    | ("-inputstate"|"-is") :: []       -> usage ()
-
-    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
-    | "-load-ml-object" :: []       -> usage ()
-
-    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
-    | "-load-ml-source" :: []       -> usage ()
-
-    | ("-load-vernac-source"|"-l") :: f :: rem ->
-	add_load_vernacular false f; parse rem
-    | ("-load-vernac-source"|"-l") :: []       -> usage ()
-
-    | ("-load-vernac-source-verbose"|"-lv") :: f :: rem ->
-	add_load_vernacular true f; parse rem
-    | ("-load-vernac-source-verbose"|"-lv") :: []       -> usage ()
-
-    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
-    | "-load-vernac-object" :: []       -> usage ()
-
-    | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
-	  (* À ne pas documenter : l'option 'stdout' n'étant
-	     éventuellement utile que pour le debugging... *)
-    | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
-    | "-dump-glob" :: []       -> usage ()
-    | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
-
-    | "-require" :: f :: rem -> add_require f; parse rem
-    | "-require" :: []       -> usage ()
-
-    | "-print-mod-uid" :: f :: rem -> Flags.print_mod_uid := true;
-                                      add_require f; parse rem
-
-    | "-compile" :: f :: rem -> add_compile false !glob_opt f; parse rem
-    | "-compile" :: []       -> usage ()
-
-    | "-compile-verbose" :: f :: rem -> add_compile true !glob_opt f; parse rem
-    | "-compile-verbose" :: []       -> usage ()
-
-    | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem
-    | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem
-    | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem
-
-    | "-beautify" :: rem -> make_beautify true; parse rem
+let print_where = ref false
+let print_config = ref false
 
-    | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
-    | "-unsafe" :: []       -> usage ()
+let get_slave_number = function
+  | "off" -> -1
+  | "on" -> 0
+  | s -> let n = int_of_string s in assert (n > 0); n
 
-    | "-debug" :: rem -> set_debug (); parse rem
+let get_bool opt = function
+  | "yes" -> true
+  | "no" -> false
+  | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
 
-    | "-time" :: rem -> Flags.time := true; parse rem
-
-    | "-compat" :: v :: rem ->
-        Flags.compat_version := get_compat_version v; parse rem
-    | "-compat" :: []       -> usage ()
-
-    | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem
-    | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem
-
-    | "-vm" :: rem -> use_vm := true; parse rem
-    | "-emacs" :: rem ->
-	Flags.print_emacs := true; Pp.make_pp_emacs();
-	Vernacentries.qed_display_script := false;
-        Flags.make_term_color false;
-	parse rem
-    | "-emacs-U" :: rem ->
-	warning "Obsolete option \"-emacs-U\", use -emacs instead.";	
-        Flags.make_term_color false;
-	parse ("-emacs" :: rem)
-
-    | "-coq-slaves" :: "off" :: rem -> Flags.coq_slave_mode := -1; parse rem
-    | "-coq-slaves" :: "on" :: rem -> Flags.coq_slave_mode := 0; parse rem
-
-    | "-coq-slaves" :: n :: rem -> (* internal use *)
-        assert (int_of_string n > 0);
-        Flags.coq_slave_mode := int_of_string n;
-        parse rem
-
-    | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
-
-    | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
-    | "-coqlib" :: [] -> usage ()
-
-    | "-where" :: _ ->
-        print_endline (Envars.coqlib ~fail:Errors.error);
-        exit (if !filter_opts then 2 else 0)
-
-    | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0)
-
-    | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
-
-    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-
-    | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0)
-
-    | "-init-file" :: f :: rem -> set_rcfile f; parse rem
-    | "-init-file" :: []       -> usage ()
-
-    | "-notactics" :: rem ->
-	warning "Obsolete option \"-notactics\".";
-	remove_top_ml (); parse rem
-
-    | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
-
-    | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
-
-    | "-xml" :: rem -> Flags.xml_export := true; parse rem
-
-    | "-output-context" :: rem -> output_context := true; parse rem
-
-    (* Scanned in Flags. *)
-    | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
-    | "-v8" :: rem -> parse rem
-
-    | "-ideslave" :: rem -> Flags.ide_slave := true; parse rem
-
-    | "-filteropts" :: rem -> filter_opts := true; parse rem
-
-    | "-color" :: rem -> Flags.make_term_color true; parse rem
-
-    | "-no-native-compiler" :: rem -> no_native_compiler := true; parse rem
-
-    | s :: rem ->
-      if !filter_opts then
-       s :: (parse rem)
-      else
-       (prerr_endline ("Don't know what to do with " ^ s); usage ())
+let parse_args arglist =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse () = match !args with
+  | [] -> List.rev !extras
+  | opt :: rem ->
+    args := rem;
+    let next () = match rem with
+      | x::rem -> args := rem; x
+      | [] -> error_missing_arg opt
+    in
+    begin match opt with
+
+    (* Complex options with many args *)
+    |"-I"|"-include" ->
+      begin match rem with
+      | d :: "-as" :: p :: rem -> set_include d p; args := rem
+      | d :: "-as" :: [] -> error_missing_arg "-as"
+      | d :: rem -> set_default_include d; args := rem
+      | [] -> error_missing_arg opt
+      end
+    |"-R" ->
+      begin match rem with
+      | d :: "-as" :: p :: rem -> set_rec_include d p; args := rem
+      | d :: "-as" :: [] -> error_missing_arg "-as"
+      | d :: p :: rem -> set_rec_include d p; args := rem
+      | _ -> error_missing_arg opt
+      end
+
+    (* Options with one arg *)
+    |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
+    |"-coq-slaves" -> Flags.coq_slave_mode := (get_slave_number (next ()))
+    |"-compat" -> Flags.compat_version := get_compat_version (next ())
+    |"-compile" -> add_compile false (next ())
+    |"-compile-verbose" -> add_compile true (next ())
+    |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
+    |"-exclude-dir" -> exclude_search_in_dirname (next ())
+    |"-init-file" -> set_rcfile (next ())
+    |"-inputstate"|"-is" -> set_inputstate (next ())
+    |"-load-ml-object" -> Mltop.dir_ml_load (next ())
+    |"-load-ml-source" -> Mltop.dir_ml_use (next ())
+    |"-load-vernac-object" -> add_vernac_obj (next ())
+    |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
+    |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
+    |"-outputstate" -> set_outputstate (next ())
+    |"-print-mod-uid" -> Flags.print_mod_uid := true; add_require (next ())
+    |"-require" -> add_require (next ())
+    |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
+    |"-unsafe" -> add_unsafe (next ())
+    |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
+
+    (* Options with zero arg *)
+    |"-batch" -> set_batch_mode ()
+    |"-beautify" -> make_beautify true
+    |"-boot" -> boot := true; no_load_rc ()
+    |"-color" -> Flags.make_term_color true
+    |"-config"|"--config" -> print_config := true
+    |"-debug" -> set_debug ()
+    |"-dont-load-proofs" -> Flags.load_proofs := Flags.Dont
+    |"-emacs" -> set_emacs ()
+    |"-filteropts" -> filter_opts := true
+    |"-force-load-proofs" -> Flags.load_proofs := Flags.Force
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+    |"-ideslave" -> Flags.ide_slave := true
+    |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+    |"-just-parsing" -> Vernac.just_parsing := true
+    |"-lazy-load-proofs" -> Flags.load_proofs := Flags.Lazy
+    |"-m"|"--memory" -> memory_stat := true
+    |"-noinit"|"-nois" -> load_init := false
+    |"-no-compat-notations" -> no_compat_ntn := true
+    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
+    |"-no-native-compiler" -> no_native_compiler := true
+    |"-notop" -> unset_toplevel_name ()
+    |"-output-context" -> output_context := true
+    |"-q" -> no_load_rc ()
+    |"-quality" -> term_quality := true; no_load_rc ()
+    |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-time" -> Flags.time := true
+    |"-unicode" -> add_require "Utf8_core"
+    |"-v"|"--version" -> Usage.version (exitcode ())
+    |"-verbose-compat-notations" -> verb_compat_ntn := true
+    |"-vm" -> use_vm := true
+    |"-where" -> print_where := true
+    |"-xml" -> Flags.xml_export := true
+
+    (* Deprecated options *)
+    |"-byte" -> warning "option -byte deprecated, call with .byte suffix"
+    |"-opt" -> warning "option -opt deprecated, call with .opt suffix"
+    |"-full" -> warning "option -full deprecated"
+    |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml ()
+    |"-emacs-U" ->
+      warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs ()
+    |"-v7" -> error "This version of Coq does not support v7 syntax"
+    |"-v8" -> warning "Obsolete option \"-v8\"."
+
+    (* Unknown option *)
+    | s -> extras := s :: !extras
+    end;
+    parse ()
   in
   try
-    parse arglist
+    parse ()
   with
     | UserError(_, s) as e ->
       if is_empty s then exit 1
@@ -376,9 +337,16 @@ let init arglist =
   Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic";
   begin
     try
-      let foreign_args = parse_args arglist in
-      if !filter_opts then
-        (print_string (String.concat "\n" foreign_args); exit 0);
+      let extras = parse_args arglist in
+      if not (List.is_empty extras) && not !filter_opts then begin
+        prerr_endline ("Don't know what to do with " ^ String.concat " " extras);
+        prerr_endline "See --help for the list of supported options";
+        exit 1
+      end;
+      Envars.set_coqlib Errors.error;
+      if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ()));
+      if !print_config then (Usage.print_config (); exit (exitcode ()));
+      if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
       if !Flags.ide_slave then begin
         Flags.make_silent true;
         Ide_slave.init_stdout ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 1bfc8f701..e9e576962 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -94,7 +94,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 ~fail:Errors.error);
+  Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
   Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
   Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
   Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;