- **Changed:**
  The warning raised when a trailing implicit is declared to be non-maximally
  inserted (with the command :cmd:`Arguments`) has been turned into an error.
  This was deprecated since Coq 8.10
  (`#11368 <https://github.com/coq/coq/pull/11368>`_,
  by SimonBoulier).