doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst


1
2
3
4
5
6

- **Removed:**
  Deprecated flag ``Bracketing Last Introduction Pattern`` affecting the
  behavior of trailing disjunctive introduction patterns is
  definitively removed
  (`#13509 <https://github.com/coq/coq/pull/13509>`_,
  by Hugo Herbelin).