diff options
| author | Théo Zimmermann | 2019-10-22 11:20:07 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-28 10:04:32 +0100 |
| commit | fbdde37d9d7d2fce7fe9b7035ad0e8efa7799dff (patch) | |
| tree | a6d68fd1a86a6e6adbae7d6dcf0e76f09425efe5 /doc/changelog/08-tools | |
| parent | 570018fe2c37eee1f87d509037162768bffe6366 (diff) | |
[changelog] Add types to changelog entries.
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
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). |