diff options
Diffstat (limited to 'doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst')
| -rw-r--r-- | doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst index 5393fb3d8c..a8d4fc6ed2 100644 --- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -1 +1,6 @@ -- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin). +- **Fixed:** + Different interpretations in different scopes of the same notation + string can now be associated to different printing formats (`#10832 + <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, + fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ + and `#7766 <https://github.com/coq/coq/issues/7766>`_). |