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/coqc.ml | |
| 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/coqc.ml')
| -rw-r--r-- | toplevel/coqc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index a403640149..b7af66b2ee 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -44,7 +44,7 @@ coqc specific options:\ let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files (opts,stm_opts) copts injections; + Ccompile.compile_file opts stm_opts copts injections; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) |