aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
blob: 41bc3329c1e82c31e15c219463224f8b186bd5de (plain)
1
2
3
4
5
- **Fixed:**
  Ltac2 notations now correctly take into account their assigned level
  (`#14094 <https://github.com/coq/coq/pull/14094>`_,
  fixes `#11866 <https://github.com/coq/coq/issues/11866>`_,
  by Pierre-Marie Pédrot).