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/07-commands-and-options | |
| 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/07-commands-and-options')
8 files changed, 18 insertions, 11 deletions
diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst index 1c91800c65..cd94bb0513 100644 --- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -1,4 +1,5 @@ -- Deprecated flag `Refine Instance Mode` has been removed. +- **Removed:** + Deprecated flag `Refine Instance Mode` (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 <https://github.com/coq/coq/issues/3890>`_ and `#4638 diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst index c69cda9656..366f799c59 100644 --- a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst +++ b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst @@ -1,2 +1,3 @@ -- Remove undocumented :n:`Instance : !@type` syntax +- **Removed:** + Undocumented :n:`Instance : !@type` syntax (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst index 7fdeb632b4..ee870df607 100644 --- a/doc/changelog/07-commands-and-options/10277-no-show-script.rst +++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst @@ -1,2 +1,3 @@ -- Remove ``Show Script`` command (deprecated since 8.10) +- **Removed:** + Deprecated ``Show Script`` command (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst index ef7adde801..7dc7def4b3 100644 --- a/doc/changelog/07-commands-and-options/10291-typing-flags.rst +++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst @@ -1,4 +1,5 @@ -- Adding unsafe commands to enable/disable guard checking, positivity checking +- **Added:** + Unsafe commands to enable/disable guard checking, positivity checking and universes checking (providing a local `-type-in-type`). - See :ref:`controlling-typing-flags`. + See :ref:`controlling-typing-flags` (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst index ba71e1c337..af38008a88 100644 --- a/doc/changelog/07-commands-and-options/10476-fix-export.rst +++ b/doc/changelog/07-commands-and-options/10476-fix-export.rst @@ -1,5 +1,6 @@ -- Fix two bugs in `Export`. This can have an impact on the behavior of the - `Import` command on libraries. `Import A` when `A` imports `B` which exports - `C` was importing `C`, whereas `Import` is not transitive. Also, after +- **Fixed:** + Two bugs in :cmd:`Export`. This can have an impact on the behavior of the + :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports + `C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after `Import A B`, the import of `B` was sometimes incomplete. (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst index 580e808baa..a17f1704fe 100644 --- a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst +++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst @@ -1,4 +1,5 @@ -- Update output generated by :flag:`Printing Dependent Evars Line` flag +- **Changed:** + Output generated by :flag:`Printing Dependent Evars Line` flag used by the Prooftree tool in Proof General. (`#10489 <https://github.com/coq/coq/pull/10489>`_, closes `#4504 <https://github.com/coq/coq/issues/4504>`_, diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst index c1df728c5c..69a9c40c3c 100644 --- a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -1,4 +1,5 @@ -- Optionally highlight the differences between successive proof steps in the +- **Added:** + Optionally highlight the differences between successive proof steps in the :cmd:`Show Proof` command. Experimental; only available in coqtop and Proof General for now, may be supported in other IDEs in the future. diff --git a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst index 283c44fda6..58c53e3b1d 100644 --- a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst +++ b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst @@ -1,4 +1,4 @@ -- Removed legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` +- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` which were undocumented, broken variants of :cmd:`Add LoadPath`, :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath` (`#11187 <https://github.com/coq/coq/pull/11187>`_, |