From 1cffe2f00d91bc9739b40887eb36f4bbad761c5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Feb 2021 19:25:53 +0100 Subject: [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 --- doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst (limited to 'doc') diff --git a/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst new file mode 100644 index 0000000000..e48b772f01 --- /dev/null +++ b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst @@ -0,0 +1,6 @@ +- **Changed:** + `coqc` now enforces that at most a single `.v` file can be passed in + the command line. Support for multiple `.v` files in the form of + `coqc f1.v f2.v` didn't properly work in 8.13, tho it was accepted. + (`#13876 `_, + by Emilio Jesus Gallego Arias). -- cgit v1.2.3