- **Changed:**
  More systematic checks that occurrences of an :n:`at` clause are
  valid in tactics such as :tacn:`rewrite` or :tacn:`pattern`
  (`#13568 <https://github.com/coq/coq/pull/13568>`_,
  fixes `#13566 <https://github.com/coq/coq/issues/13566>`_,
  by Hugo Herbelin).