coq/doc/changelog/08-cli-tools, branch master The formal proof system [coqdep] error on non-existent and unreadable files 2021-04-12T19:31:12+00:00 Hendrik Tews 2021-03-28T20:06:03+00:00 e1793962bebf1401026ed961ecc15b7eb60d57f5 Print an error message and return non-zero status for non-existing or unreadable files. Unknown options produce a warning and are otherwise ignored. Fixes #14023 
Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023
Adding change log for #13624. 2021-04-04T09:01:25+00:00 Hugo Herbelin 2020-12-12T11:22:18+00:00 950015d13ceb0c65c2eda42578788c8fe7ea31f1 






[coqc] Don't allow to pass more than one file to coqc
2021-02-26T21:57:53+00:00

Emilio Jesus Gallego Arias

2021-02-18T18:25:53+00:00

1cffe2f00d91bc9739b40887eb36f4bbad761c5f

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





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







Changelog for #13822
2021-02-04T14:30:30+00:00

Gaëtan Gilbert

2021-02-04T14:29:08+00:00

7aaf8248539f9e75ff02e57b5b3142d0de6c20e9












Clarify changelog categories.
2020-12-11T09:02:30+00:00

Théo Zimmermann

2020-12-11T09:02:27+00:00

1605ae821f151f1e4b4edab9a0dded02cb91eebf

For readers of the changelog: title "Tools" become "Command-line tools".
For developers: changelog categories 07 and 08 are disambiguated.





For readers of the changelog: title "Tools" become "Command-line tools".
For developers: changelog categories 07 and 08 are disambiguated.