diff options
| author | SimonBoulier | 2020-03-12 11:12:48 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-03-12 11:22:50 +0100 |
| commit | 0626df49c72badbb51d2f31eb7d1b1fee22c2638 (patch) | |
| tree | debcadff0552ccea9915d31b6d64cde107765d76 | |
| parent | 6251f1b0b453a90c1c2a993c6980c1f40bfb2de7 (diff) | |
Add changelog
| -rw-r--r-- | doc/changelog/07-commands-and-options/11795-print_implicit_args.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst new file mode 100644 index 0000000000..5b0cdb5914 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst @@ -0,0 +1,5 @@ +- **Added:** + Several commands (`Search`, `About`, ...) now print the implicit arguments + in brackets when printing types. + (`#11795 <https://github.com/coq/coq/pull/11795>`_, + by SimonBoulier). |