[toplevel] Split interactive toplevel and compiler binaries.

We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.

Thus, `coqtop -compile` will emit a warning and call `coqc`.

We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.

This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.

1 files changed, 14 insertions, 4 deletions

diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index c95d0aca55..300a7a039b 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -12,14 +12,24 @@
     [init] is used to do custom command line argument parsing.
     [run] launches a custom toplevel.
 *)
-open Coqargs
+
+type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
 
 type custom_toplevel =
-  { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list
-  ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit
-  ; opts : Coqargs.coq_cmdopts
+  { init : init_fn
+  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+  ; opts : Coqargs.t
   }
 
+(** [init_toplevel ~help ~init custom_init arg_list]
+    Common Coq initialization and argument parsing *)
+val init_toplevel
+  :  help:(unit -> unit)
+  -> init:Coqargs.t
+  -> init_fn
+  -> string list
+  -> Coqargs.t * string list
+
 val coqtop_toplevel : custom_toplevel
 
 (** The Coq main module. [start custom] will parse the command line,