From fbdde37d9d7d2fce7fe9b7035ad0e8efa7799dff Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 22 Oct 2019 11:20:07 +0200 Subject: [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. --- doc/changelog/08-tools/08642-vos-files.rst | 3 ++- doc/changelog/08-tools/10245-require-command-line.rst | 3 ++- doc/changelog/08-tools/10947-coq-makefile-dep.rst | 3 ++- doc/changelog/08-tools/11068-coqbin-noslash.rst | 2 +- 4 files changed, 7 insertions(+), 4 deletions(-) (limited to 'doc/changelog/08-tools') 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 `..d` in the `coq_makefile` +- **Changed:** + Renamed `VDFILE` from `.coqdeps.d` to `..d` in the `coq_makefile` utility, where `` 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 `_, by Gaëtan Gilbert). -- cgit v1.2.3