diff options
Diffstat (limited to 'doc/changelog/03-notations/12163-fix-12159.rst')
| -rw-r--r-- | doc/changelog/03-notations/12163-fix-12159.rst | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst deleted file mode 100644 index 978ed561dd..0000000000 --- a/doc/changelog/03-notations/12163-fix-12159.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Fixed:** - Numeral Notations now play better with multiple scopes for the same - inductive type. Previously, when multiple numeral notations were defined - for the same inductive, only the last one was considered for - printing. Now, among the notations that are usable for printing and either - have a scope delimiter or are open, the selection is made according - to the order of open scopes, or according to the last defined - notation if no appropriate scope is open - (`#12163 <https://github.com/coq/coq/pull/12163>`_, - fixes `#12159 <https://github.com/coq/coq/pull/12159>`_, - by Pierre Roux, review by Hugo Herbelin and Jason Gross). |