aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst
blob: fc909e7a1d778f0eebc9f9cdf944260f02e91653 (plain)
1
2
3
4
5
6
7
8
- **Fixed:**
  Issues in the presence of notations recursively referring to another
  applicative notations, such as missing scope propagation, or failure
  to use a notation for printing
  (`#12960 <https://github.com/coq/coq/pull/12960>`_,
  fixes `#9403 <https://github.com/coq/coq/issues/9403>`_
  and `#10803 <https://github.com/coq/coq/issues/10803>`_,
  by Hugo Herbelin).