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/02-specification-language/10985-about-arguments.rst | |
| 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/02-specification-language/10985-about-arguments.rst')
| -rw-r--r-- | doc/changelog/02-specification-language/10985-about-arguments.rst | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst index 1e05b0b0fe..0faaf95e6c 100644 --- a/doc/changelog/02-specification-language/10985-about-arguments.rst +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -1,5 +1,6 @@ -- The output of the :cmd:`Print` and :cmd:`About` commands has - changed. Arguments meta-data is now displayed as the corresponding +- **Changed:** + Output of the :cmd:`Print` and :cmd:`About` commands. + Arguments meta-data is now displayed as the corresponding :cmd:`Arguments <Arguments (implicits)>` command instead of the human-targeted prose used in previous Coq versions. (`#10985 <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). |