From 103f59ed6b8174ed9359cb11c909f1b2219390c9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 9 Oct 2018 23:02:28 +0200
Subject: [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.
---
 toplevel/ccompile.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel/ccompile.mli')

diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 757c91c408..29a76eb966 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -10,10 +10,10 @@
 
 (** [load_init_vernaculars opts ~state] Load vernaculars from
    the init (rc) file *)
-val load_init_vernaculars : Coqargs.coq_cmdopts -> state:Vernac.State.t-> Vernac.State.t
+val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
 
 (** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.coq_cmdopts -> unit
+val compile_files : Coqargs.t -> Coqcargs.t -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
-val do_vio : Coqargs.coq_cmdopts -> unit
+val do_vio : Coqargs.t -> Coqcargs.t -> unit
-- 
cgit v1.2.3