diff options
| author | Hugo Herbelin | 2019-11-12 22:12:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:07 +0100 |
| commit | a91c22fcfd5df6153cc9f1b1b4e3d9840055bf0d (patch) | |
| tree | 7a2480c669f10cc14fc5e2a766a58d6ab0ef23fe /doc | |
| parent | 8364b7fea91a11ad07d94057f3a5a938b9524d81 (diff) | |
Adding change log for #10832.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst | 1 |
1 files changed, 1 insertions, 0 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 new file mode 100644 index 0000000000..5393fb3d8c --- /dev/null +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -0,0 +1 @@ +- 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). |