blob: 1e05b0b0fec6275310df6f9d7ae4d3a03323a6c0 (
plain)
1
2
3
4
5
|
- The output of the :cmd:`Print` and :cmd:`About` commands has
changed. 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).
|
