blob: 0faaf95e6c8491564ed1d7e76fd65a5ccd94ceef (
plain)
1
2
3
4
5
6
|
- **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).
|
