- **Fixed**
  Efficiency regression introduced by  PR `#9725 <https://github.com/coq/coq/pull/9725>`_.
  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
  and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson).