1 files changed, 65 insertions, 0 deletions
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
new file mode 100644
index 00000000..de9b6a68
--- /dev/null
+++ b/toplevel/coqargs.mli
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+type color = [`ON | `AUTO | `OFF]
+
+type coq_cmdopts = {
+
+  load_init   : bool;
+  load_rcfile : bool;
+  rcfile      : string option;
+
+  ml_includes : string list;
+  vo_includes : (string * Names.DirPath.t * bool) list;
+  vo_requires : (string * string option * bool option) list;
+
+  (* Fuse these two? Currently, [batch_mode] is only used to
+     distinguish coqc / coqtop in help display. *)
+  batch_mode : bool;
+  compilation_mode : compilation_mode;
+
+  toplevel_name : Names.DirPath.t;
+  toploop : string option;
+
+  compile_list: (string * bool) list;  (* bool is verbosity  *)
+  compilation_output_name : string option;
+
+  load_vernacular_list : (string * bool) list;
+
+  vio_checking: bool;
+  vio_tasks   : (int list * string) list;
+  vio_files   : string list;
+  vio_files_j : int;
+
+  color : color;
+
+  impredicative_set : Declarations.set_predicativity;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  time        : bool;
+
+  filter_opts : bool;
+
+  glob_opt    : bool;
+
+  memory_stat : bool;
+  print_tags  : bool;
+  print_where : bool;
+  print_config: bool;
+  output_context : bool;
+
+  inputstate  : string option;
+  outputstate : string option;
+
+}
+
+val parse_args : string list -> coq_cmdopts * string list
+val exitcode : coq_cmdopts -> int