diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
| commit | c45b7e41a1caa4d5ec4785c2bf323bdd11ad8d2e (patch) | |
| tree | 86d2847ee9b7c34c602fe41715afa171e41ffeba /doc/changelog | |
| parent | 3f7eb03c82c9db9673cc8ae9c81c8f9132003751 (diff) | |
| parent | 779b8a105e3e06bde673c1abc4f918101c113fe2 (diff) | |
Merge PR #11261: Use implicit types for printing (granting wish #10366).
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst new file mode 100644 index 0000000000..51818c666b --- /dev/null +++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, + unset the :flag:`Printing Use Implicit Types` flag + (`#11261 <https://github.com/coq/coq/pull/11261>`_, + by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). |