doc/changelog/03-notations/11113-remove-compat.rst


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).