diff options
Diffstat (limited to 'doc/changelog/08-tools')
4 files changed, 7 insertions, 4 deletions
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst index f612096880..83937390fc 100644 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -1,4 +1,5 @@ -- `coqc` now provides the ability to generate compiled interfaces. +- **Added:** + `coqc` now provides the ability to generate compiled interfaces. Use `coqc -vos foo.v` to skip all opaque proofs during the compilation of `foo.v`, and output a file called `foo.vos`. This feature is experimental. It enables working on a Coq file without the need to diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst index 54417077f5..ca871bbf6b 100644 --- a/doc/changelog/08-tools/10245-require-command-line.rst +++ b/doc/changelog/08-tools/10245-require-command-line.rst @@ -1,4 +1,5 @@ -- Add command line options `-require-import`, `-require-export`, +- **Added:** + Command-line options `-require-import`, `-require-export`, `-require-import-from` and `-require-export-from`, as well as their shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate confusing command line option `-require` diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst index f620b32cb8..c59f1312d1 100644 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst @@ -1,4 +1,5 @@ -- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` +- **Changed:** + Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` utility, where `<CoqMakefile>` is the name of the output file given by the `-o` option. In this way two generated makefiles can coexist in the same directory. diff --git a/doc/changelog/08-tools/11068-coqbin-noslash.rst b/doc/changelog/08-tools/11068-coqbin-noslash.rst index c2c8f4df31..cd48f9d606 100644 --- a/doc/changelog/08-tools/11068-coqbin-noslash.rst +++ b/doc/changelog/08-tools/11068-coqbin-noslash.rst @@ -1,3 +1,3 @@ -- ``coq_makefile`` now supports environment variable ``COQBIN`` with +- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with no ending ``/`` character (`#11068 <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). |