diff options
| author | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
| commit | 3ae4231d30edfa928595b6fa886ce6df1a495089 (patch) | |
| tree | d6c1d749e6435570e3437f012aad8e6d6797c432 /doc | |
| parent | 1d8698e97dee385151ef92efd924560b296f8d50 (diff) | |
| parent | ea16c402392722a44bf2227aef7ff73faef70d3a (diff) | |
Merge PR #11795: Print implicit arguments in types of references
Ack-by: herbelin
Diffstat (limited to 'doc')
| -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). |