aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/03-notations/11113-remove-compat.rst
blob: 3bcdd3dd6f6f2c507f1b04128fcc6a8ae47d9f38 (plain)
1
2
3
4
- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation`
  and :cmd:`Infix` commands
  (`#11113 <https://github.com/coq/coq/pull/11113>`_,
  by Théo Zimmermann, with help from Jason Gross).