A classification of command line options.

A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
  another query (this allows to get rid of the "exitcode" hack)

9 files changed, 297 insertions, 218 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 605db74836..d8a3dbb4bb 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -22,9 +22,9 @@ let fatal_error msg =
 (******************************************************************************)
 
 let load_init_file opts ~state =
-  if opts.load_rcfile then
+  if opts.pre.load_rcfile then
     Topfmt.(in_phase ~phase:LoadingRcFile) (fun () ->
-        Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) ()
+        Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
   else begin
     Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
     state
@@ -39,7 +39,7 @@ let load_vernacular opts ~state =
       if !Flags.beautify
       then Flags.with_option Flags.beautify_file load_vernac f_in
       else load_vernac s
-    ) state (List.rev opts.load_vernacular_list)
+    ) state (List.rev opts.pre.load_vernacular_list)
 
 let load_init_vernaculars opts ~state =
   let state = load_init_file opts ~state in
@@ -102,8 +102,8 @@ let compile opts copts ~echo ~f_in ~f_out =
   in
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
-  let stm_options = opts.stm_flags in
-  let output_native_objects = match opts.native_compiler with
+  let stm_options = opts.config.stm_flags in
+  let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
   in
   match copts.compilation_mode with
@@ -118,7 +118,7 @@ let compile opts copts ~echo ~f_in ~f_out =
           Stm.{ doc_type = VoDoc long_f_dot_vo;
                 iload_path; require_libs; stm_options;
               } in
-      let state = { doc; sid; proof = None; time = opts.time } in
+      let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
@@ -164,7 +164,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                 iload_path; require_libs; stm_options;
               } in
 
-      let state = { doc; sid; proof = None; time = opts.time } in
+      let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 7e3759f177..e47fbf2921 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -40,52 +40,70 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type option_command = OptionSet of string option | OptionUnset
 
-type t = {
+type coqargs_logic_config = {
+  impredicative_set : Declarations.set_predicativity;
+  indices_matter    : bool;
+  toplevel_name     : Stm.interactive_top;
+  allow_sprop       : bool;
+  cumulative_sprop  : bool;
+}
 
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  diffs_set   : bool;
+  time        : bool;
+  glob_opt    : bool;
+  print_emacs : bool;
+  set_options : (Goptions.option_name * option_command) list;
+}
+
+type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
-  rcfile      : string option;
 
   ml_includes : Loadpath.coq_path list;
   vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
-  toplevel_name : Stm.interactive_top;
-
   load_vernacular_list : (string * bool) list;
-  batch : bool;
 
-  color : color;
+  inputstate  : string option;
+}
 
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter : bool;
-  enable_VM : bool;
-  native_compiler : native_compiler;
-  allow_sprop : bool;
-  cumulative_sprop : bool;
+type coqargs_base_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of (unit -> unit)
 
-  set_options : (Goptions.option_name * option_command) list;
-
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  diffs_set   : bool;
-  time        : bool;
+type coqargs_queries = {
+  queries : coqargs_base_query list;
+  filteropts : bool;
+}
 
-  filter_opts : bool;
+type coqargs_interactive = Interactive | Batch
 
-  glob_opt    : bool;
+type coqargs_main =
+  | Queries of coqargs_queries
+  | Run of coqargs_interactive
 
+type coqargs_post = {
   memory_stat : bool;
-  print_tags  : bool;
-  print_where : bool;
-  print_config: bool;
   output_context : bool;
+}
 
-  print_emacs : bool;
-
-  inputstate  : string option;
-
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
 }
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
@@ -95,69 +113,77 @@ let default_native =
   then NativeOn {ondemand=true}
   else NativeOff
 
-let default = {
-
-  load_init   = true;
-  load_rcfile = true;
-  rcfile      = None;
-
-  ml_includes = [];
-  vo_includes = [];
-  vo_requires = [];
-
-  toplevel_name = Stm.TopLogical default_toplevel;
-
-  load_vernacular_list = [];
-  batch = false;
-
-  color = `AUTO;
-
+let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
-  enable_VM = true;
-  native_compiler = default_native;
+  toplevel_name = Stm.TopLogical default_toplevel;
   allow_sprop = false;
   cumulative_sprop = false;
+}
 
-  set_options = [];
-
+let default_config = {
+  logic        = default_logic_config;
+  rcfile       = None;
+  coqlib       = None;
+  color        = `AUTO;
+  enable_VM    = true;
+  native_compiler = default_native;
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
   time         = false;
+  glob_opt     = false;
+  print_emacs  = false;
+  set_options  = [];
+
+  (* Quiet / verbosity options should be here *)
+}
 
-  filter_opts  = false;
+let default_pre = {
+  load_init    = true;
+  load_rcfile  = true;
+  ml_includes  = [];
+  vo_includes  = [];
+  vo_requires  = [];
+  load_vernacular_list = [];
+  inputstate   = None;
+}
 
-  glob_opt     = false;
+let default_queries = {
+  queries = [];
+  filteropts = false;
+}
 
+let default_main =
+  Run Interactive
+
+let default_post = {
   memory_stat  = false;
-  print_tags   = false;
-  print_where  = false;
-  print_config = false;
   output_context = false;
+}
 
-  print_emacs = false;
-
-  (* Quiet / verbosity options should be here *)
-
-  inputstate  = None;
+let default = {
+  config = default_config;
+  pre    = default_pre;
+  main   = default_main;
+  post   = default_post;
 }
 
 (******************************************************************************)
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
+  Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }}
 
 let add_vo_include opts unix_path coq_path implicit =
   let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
-  { opts with vo_includes = {
+  { opts with pre = { opts.pre with vo_includes = {
         recursive = true;
-        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.vo_includes }
+        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
-  { opts with vo_requires = (d, p, export) :: opts.vo_requires }
+  { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
 
 let add_compat_require opts v =
   match v with
@@ -166,19 +192,45 @@ let add_compat_require opts v =
   | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
 
 let add_load_vernacular opts verb s =
-  { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list }
+  { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
 
 (** Options for proof general *)
 let set_emacs opts =
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `EMACS; print_emacs = true }
+  { opts with config = { opts.config with color = `OFF; print_emacs = true }}
+
+let set_logic f oval =
+  { oval with config = { oval.config with logic = f oval.config.logic }}
 
 let set_color opts = function
-| "yes" | "on" -> { opts with color = `ON }
-| "no" | "off" -> { opts with color = `OFF }
-| "auto" -> { opts with color = `AUTO }
-| _ ->
-  error_wrong_arg ("Error: on/off/auto expected after option color")
+  | "yes" | "on" -> { opts with config = { opts.config with color = `ON }}
+  | "no" | "off" -> { opts with config = { opts.config with color = `OFF }}
+  | "auto" -> { opts with config = { opts.config with color = `AUTO }}
+  | _ ->
+    error_wrong_arg ("Error: on/off/auto expected after option color")
+
+let set_batch opts =
+  { opts with main = match opts.main with
+  | Run _ -> Run Batch
+  | Queries _ as x -> x }
+
+let add_query { queries; filteropts } q =
+  { queries = queries@[q]; filteropts }
+
+let set_query opts q =
+  { opts with main = match opts.main with
+  | Run _ -> Queries (add_query default_queries q)
+  | Queries queries -> Queries (add_query queries q)
+  }
+
+let add_filteropts { queries } =
+  { queries; filteropts = true }
+
+let set_filteropts opts =
+  { opts with main = match opts.main with
+  | Run _ -> Queries (add_filteropts default_queries)
+  | Queries queries -> Queries (add_filteropts queries)
+  }
 
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
@@ -190,9 +242,7 @@ let warn_deprecated_simple_require =
 
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
-  { opts with inputstate = Some s }
-
-let exitcode opts = if opts.filter_opts then 2 else 0
+  { opts with pre = { opts.pre with inputstate = Some s }}
 
 (******************************************************************************)
 (* Parsing helpers                                                            *)
@@ -320,54 +370,54 @@ let parse_args ~help ~init arglist : t * string list =
 
     (* Options with one arg *)
     |"-coqlib" ->
-      Envars.set_user_coqlib (next ());
-      oval
+      { oval with config = { oval.config with coqlib = Some (next ())
+      }}
 
     |"-async-proofs" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
-      }}
+      }}}
     |"-async-proofs-j" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
-      }}
+      }}}
     |"-async-proofs-cache" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-tac-j" ->
       let j = get_int opt (next ()) in
       if j <= 0 then begin
         error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
       end;
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_n_tacworkers = j
-      }}
+      }}}
 
     |"-async-proofs-worker-priority" ->
       CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ());
       oval
 
     |"-async-proofs-private-flags" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
-      }}
+      }}}
 
     |"-async-proofs-tactic-error-resilience" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-command-error-resilience" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-delegation-threshold" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
-      }}
+      }}}
 
     |"-worker-id" -> set_worker_id opt (next ()); oval
 
@@ -378,7 +428,7 @@ let parse_args ~help ~init arglist : t * string list =
 
     |"-dump-glob" ->
       Dumpglob.dump_into_file (next ());
-      { oval with glob_opt = true }
+      { oval with config = { oval.config with glob_opt = true }}
 
     |"-feedback-glob" ->
       Dumpglob.feedback_glob (); oval
@@ -387,7 +437,7 @@ let parse_args ~help ~init arglist : t * string list =
       System.exclude_directory (next ()); oval
 
     |"-init-file" ->
-      { oval with rcfile = Some (next ()); }
+      { oval with config = { oval.config with rcfile = Some (next ()); }}
 
     |"-inputstate"|"-is" ->
       set_inputstate oval (next ())
@@ -441,10 +491,10 @@ let parse_args ~help ~init arglist : t * string list =
       let topname = Libnames.dirpath_of_string (next ()) in
       if Names.DirPath.is_empty topname then
         CErrors.user_err Pp.(str "Need a non empty toplevel module name");
-      { oval with toplevel_name = Stm.TopLogical topname }
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}}
 
     |"-topfile" ->
-      { oval with toplevel_name = Stm.TopPhysical (next()) }
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}}
 
     |"-main-channel" ->
       Spawned.main_channel := get_host_port opt (next()); oval
@@ -462,7 +512,7 @@ let parse_args ~help ~init arglist : t * string list =
         oval
 
     |"-bytecode-compiler" ->
-      { oval with enable_VM = get_bool opt (next ()) }
+      { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }}
 
     |"-native-compiler" ->
 
@@ -479,68 +529,67 @@ let parse_args ~help ~init arglist : t * string list =
         | _ ->
           error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler")
       in
-      { oval with native_compiler }
+      { oval with config = { oval.config with native_compiler }}
 
     | "-set" ->
       let opt = next() in
       let opt, v = parse_option_set opt in
-      { oval with set_options = (opt, OptionSet v) :: oval.set_options }
+      { oval with config = { oval.config with set_options = (opt, OptionSet v) :: oval.config.set_options }}
 
     | "-unset" ->
       let opt = next() in
       let opt = to_opt_key opt in
-      { oval with set_options = (opt, OptionUnset) :: oval.set_options }
+      { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }}
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
     |"-async-proofs-never-reopen-branch" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_never_reopen_branch = true
-      }}
+      }}}
     |"-batch" ->
       Flags.quiet := true;
-      { oval with batch = true }
+      set_batch oval
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
-    |"-config"|"--config" -> { oval with print_config = true }
+    |"-config"|"--config" -> set_query oval PrintConfig
     |"-debug" -> Coqinit.set_debug (); oval
     |"-diffs" -> let opt = next () in
                   if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
                     Proof_diffs.write_diffs_option opt
                   else
                     error_wrong_arg "Error: on|off|removed expected after -diffs";
-                  { oval with diffs_set = true }
+                  { oval with config = { oval.config with diffs_set = true }}
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
-    |"-filteropts" -> { oval with filter_opts = true }
+    |"-filteropts" -> set_filteropts oval
     |"-impredicative-set" ->
-      { oval with impredicative_set = Declarations.ImpredicativeSet }
-    |"-allow-sprop" -> { oval with allow_sprop = true }
-    |"-disallow-sprop" -> { oval with allow_sprop = false }
-    |"-sprop-cumulative" -> { oval with cumulative_sprop = true }
-    |"-indices-matter" -> { oval with indices_matter = true }
-    |"-m"|"--memory" -> { oval with memory_stat = true }
-    |"-noinit"|"-nois" -> { oval with load_init = false }
-    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true }
-    |"-output-context" -> { oval with output_context = true }
+      set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
+    |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval
+    |"-disallow-sprop" -> set_logic (fun o -> { o with allow_sprop = false }) oval
+    |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval
+    |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
+    |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
+    |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }}
+    |"-output-context" -> { oval with post = { oval.post with output_context = true }}
     |"-profile-ltac" -> Flags.profile_ltac := true; oval
-    |"-q" -> { oval with load_rcfile = false; }
+    |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
     |"-quiet"|"-silent" ->
       Flags.quiet := true;
       Flags.make_warn false;
       oval
-    |"-list-tags" -> { oval with print_tags = true }
-    |"-time" -> { oval with time = true }
+    |"-list-tags" -> set_query oval PrintTags
+    |"-time" -> { oval with config = { oval.config with time = true }}
     |"-type-in-type" -> set_type_in_type (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
-    |"-where" -> { oval with print_where = true }
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval
-    |"-v"|"--version" -> Usage.version (exitcode oval)
-    |"-print-version"|"--print-version" ->
-      Usage.machine_readable_version (exitcode oval)
+    |"-where" -> set_query oval PrintWhere
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp (fun () -> usage help))
+    |"-v"|"--version" -> set_query oval PrintVersion
+    |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
 
     (* Unknown option *)
     | s ->
@@ -560,11 +609,11 @@ let parse_args ~help ~init arglist : t * string list =
 let prelude_data = "Prelude", Some "Coq", Some false
 
 let require_libs opts =
-  if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
+  if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
 let cmdline_load_path opts =
-  List.rev opts.vo_includes @ List.(rev opts.ml_includes)
+  List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes)
 
 let build_load_path opts =
-  Coqinit.libs_init_load_path ~load_init:opts.load_init @
+  Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
   cmdline_load_path opts
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 81f8983e98..897885997c 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -16,57 +16,76 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type option_command = OptionSet of string option | OptionUnset
 
-type t = {
+type coqargs_logic_config = {
+  impredicative_set : Declarations.set_predicativity;
+  indices_matter    : bool;
+  toplevel_name     : Stm.interactive_top;
+  allow_sprop       : bool;
+  cumulative_sprop  : bool;
+}
 
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  diffs_set   : bool;
+  time        : bool;
+  glob_opt    : bool;
+  print_emacs : bool;
+  set_options : (Goptions.option_name * option_command) list;
+}
+
+type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
-  rcfile      : string option;
 
   ml_includes : Loadpath.coq_path list;
   vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
-
-  toplevel_name : Stm.interactive_top;
+  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
-  batch : bool;
-
-  color : color;
+  inputstate  : string option;
+}
 
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter : bool;
-  enable_VM : bool;
-  native_compiler : native_compiler;
-  allow_sprop : bool;
-  cumulative_sprop : bool;
+type coqargs_base_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of (unit -> unit)
 
-  set_options : (Goptions.option_name * option_command) list;
-
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  diffs_set   : bool;
-  time        : bool;
+type coqargs_queries = {
+  queries : coqargs_base_query list;
+  filteropts : bool;
+}
 
-  filter_opts : bool;
+type coqargs_interactive = Interactive | Batch
 
-  glob_opt    : bool;
+type coqargs_main =
+  | Queries of coqargs_queries
+  | Run of coqargs_interactive
 
+type coqargs_post = {
   memory_stat : bool;
-  print_tags  : bool;
-  print_where : bool;
-  print_config: bool;
   output_context : bool;
+}
 
-  print_emacs : bool;
-
-  inputstate  : string option;
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
 }
 
 (* Default options *)
 val default : t
 
 val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
-val exitcode : t -> int
+val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
 val build_load_path : t -> Loadpath.coq_path list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index a04552e8db..7c4aded5bb 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -28,11 +28,11 @@ let coqc_main () =
   in
   let opts, extras =
     Topfmt.(in_phase ~phase:Initialization)
-      Coqtop.(init_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in
+      Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in
 
   let copts = Coqcargs.parse extras in
 
-  if not opts.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
+  if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
 
   Topfmt.(in_phase ~phase:CompilationPhase)
     Ccompile.compile_files opts copts;
@@ -47,7 +47,7 @@ let coqc_main () =
 
   flush_all();
 
-  if opts.Coqargs.output_context then begin
+  if opts.Coqargs.post.Coqargs.output_context then begin
     let sigma, env = let e = Global.env () in Evd.from_env e, e in
     Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
   end;
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4bcde566e3..f6211102e6 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -444,7 +444,7 @@ let drop_args = ref None
 let loop ~opts ~state =
   drop_args := Some opts;
   let open Coqargs in
-  print_emacs := opts.print_emacs;
+  print_emacs := opts.config.print_emacs;
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder coqloop_feed in
   if Dumpglob.dump () then begin
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 170959f2e2..22d293129e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -48,8 +48,6 @@ let print_memory_stat () =
     with _ -> ()
   end
 
-let _ = at_exit print_memory_stat
-
 let interp_set_option opt v old =
   let open Goptions in
   let err expect =
@@ -159,6 +157,22 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
+
+let print_queries opts extras q =
+  let print_query = function
+    | PrintVersion -> Usage.version ()
+    | PrintMachineReadableVersion -> Usage.machine_readable_version ()
+    | PrintWhere -> print_endline (Envars.coqlib ())
+    | PrintHelp f -> f ()
+    | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
+    | PrintTags -> print_style_tags opts.config in
+  List.iter print_query q.queries;
+  if q.filteropts then
+    if q.queries <> [] && extras <> [] then
+      error_wrong_arg "Queries are exclusive of other arguments"
+    else
+      print_string (String.concat "\n" extras)
+
 (** GC tweaking *)
 
 (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
@@ -184,6 +198,10 @@ let init_gc () =
              Gc.minor_heap_size = 33554432; (* 4M *)
              Gc.space_overhead = 120}
 
+let init_setup = function
+  | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+  | Some s -> Envars.set_user_coqlib s
+
 (** Main init routine *)
 let init_toplevel ~help ~init custom_init arglist =
   (* Coq's init process, phase 1:
@@ -199,58 +217,44 @@ let init_toplevel ~help ~init custom_init arglist =
      Basic Coq environment, load-path, plugins.
    *)
   let opts, extras = parse_args ~help ~init arglist in
-  memory_stat := opts.memory_stat;
+  if opts.post.memory_stat then at_exit print_memory_stat;
 
   (* If we have been spawned by the Spawn module, this has to be done
    * early since the master waits us to connect back *)
   Spawned.init_channels ();
-  Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-  if opts.print_where then begin
-    print_endline (Envars.coqlib ());
-    exit (exitcode opts)
-  end;
-  if opts.print_config then begin
-    Envars.print_config stdout Coq_config.all_src_dirs;
-    exit (exitcode opts)
-  end;
-  if opts.print_tags then begin
-    print_style_tags opts;
-    exit (exitcode opts)
-  end;
-  if opts.filter_opts then begin
-    print_string (String.concat "\n" extras);
-    exit 0;
-  end;
+  init_setup opts.config.coqlib;
+  (* Querying or running? *)
+  match opts.main with
+  | Queries q -> print_queries opts extras q; exit 0
+  | Run batch ->
+  (* Initialization *)
   let top_lp = Coqinit.toplevel_init_load_path () in
   List.iter Loadpath.add_coq_path top_lp;
   let opts, extras = custom_init ~opts extras in
   Mltop.init_known_plugins ();
+  (* Configuration *)
+  Global.set_engagement opts.config.logic.impredicative_set;
+  Global.set_indices_matter opts.config.logic.indices_matter;
+  Global.set_VM opts.config.enable_VM;
+  Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
+  Global.set_allow_sprop opts.config.logic.allow_sprop;
+  if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative ();
 
-  Global.set_engagement opts.impredicative_set;
-  Global.set_indices_matter opts.indices_matter;
-  Global.set_VM opts.enable_VM;
-  Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
-  Global.set_allow_sprop opts.allow_sprop;
-  if opts.cumulative_sprop then Global.make_sprop_cumulative ();
-
-  set_options opts.set_options;
+  set_options opts.config.set_options;
 
   (* Allow the user to load an arbitrary state here *)
-  inputstate opts;
+  inputstate opts.pre;
 
   (* This state will be shared by all the documents *)
   Stm.init_core ();
+  batch, opts, extras
 
-  (* Coq init process, phase 3: Stm initialization, backtracking state.
+type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
 
-     It is essential that the module system is in a consistent
-     state before we take the first snapshot. This was not
-     guaranteed in the past, but now is thanks to the STM API.
-  *)
+let init_batch_toplevel ~help ~init custom_init args =
+  let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in
   opts, extras
 
-type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
-
 type custom_toplevel =
   { init : init_fn
   ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
@@ -258,16 +262,22 @@ type custom_toplevel =
   }
 
 let init_document opts =
+  (* Coq init process, phase 3: Stm initialization, backtracking state.
+
+     It is essential that the module system is in a consistent
+     state before we take the first snapshot. This was not
+     guaranteed in the past, but now is thanks to the STM API.
+  *)
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
-  let stm_options = opts.stm_flags in
+  let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
-           { doc_type = Interactive opts.toplevel_name;
+           { doc_type = Interactive opts.config.logic.toplevel_name;
              iload_path; require_libs; stm_options;
            }) in
-  { doc; sid; proof = None; time = opts.time }
+  { doc; sid; proof = None; time = opts.config.time }
 
 let init_toploop opts =
   let state = init_document opts in
@@ -275,7 +285,7 @@ let init_toploop opts =
   state
 
 let coqtop_init ~opts extra =
-  init_color opts;
+  init_color opts.config;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
   Flags.if_verbose print_header ();
   opts, extra
@@ -289,9 +299,9 @@ let coqtop_toplevel =
 let start_coq custom =
   let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   (* Init phase *)
-  let state, opts =
+  let run_mode, state, opts =
     try
-      let opts, extras =
+      let run_mode, opts, extras =
         init_toplevel
           ~help:Usage.print_usage_coqtop ~init:default custom.init
           (List.tl (Array.to_list Sys.argv)) in
@@ -300,10 +310,12 @@ let start_coq custom =
         prerr_endline "See -help for the list of supported options";
         exit 1
       end;
-      init_toploop opts, opts
+      let state = init_toploop opts in
+      run_mode, state, opts
     with any ->
       flush_all();
       fatal_error_exn any in
   Feedback.del_feeder init_feeder;
-  if not opts.batch then custom.run ~opts ~state;
-  exit 0
+  match run_mode with
+  | Interactive -> custom.run ~opts ~state;
+  | Batch -> exit 0
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 40f569a1c8..d1f0f78355 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -23,7 +23,7 @@ type custom_toplevel =
 
 (** [init_toplevel ~help ~init custom_init arg_list]
     Common Coq initialization and argument parsing *)
-val init_toplevel
+val init_batch_toplevel
   :  help:(unit -> unit)
   -> init:Coqargs.t
   -> init_fn
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 91b3c32126..011cc34987 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -8,15 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let version ret =
+let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
     Coq_config.version Coq_config.date;
-  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version;
-  exit ret
-let machine_readable_version ret =
+  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
+
+let machine_readable_version () =
   Printf.printf "%s %s\n"
-    Coq_config.version Coq_config.caml_version;
-  exit ret
+    Coq_config.version Coq_config.caml_version
 
 (* print the usage of coqtop (or coqc) on channel co *)
 
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 1f257a5896..7d658579fd 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -8,10 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** {6 Prints the version number on the standard output and exits (with 0). } *)
+(** {6 Prints the version number on the standard output. } *)
 
-val version : int -> 'a
-val machine_readable_version : int -> 'a
+val version : unit -> unit
+val machine_readable_version : unit -> unit
 
 (** {6 Enable toploop plugins to insert some text in the usage message. } *)
 val add_to_usage : string -> string -> unit