diff options
| author | Emilio Jesus Gallego Arias | 2021-02-18 19:25:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2021-02-26 22:57:53 +0100 |
| commit | 1cffe2f00d91bc9739b40887eb36f4bbad761c5f (patch) | |
| tree | 14c339ae29c232f1b110b7f05f8e59fbeb07fc76 /toplevel/ccompile.mli | |
| parent | 1e54fe53ac47f08d7b8f13df16487b5a2639404f (diff) | |
[coqc] Don't allow to pass more than one file to coqc
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
Diffstat (limited to 'toplevel/ccompile.mli')
| -rw-r--r-- | toplevel/ccompile.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 9f3783f32e..e9e83af3ad 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -12,8 +12,8 @@ the init (rc) file *) 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.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit +(** [compile_file opts] compile file specified in [opts] *) +val compile_file : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> unit |