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