- **Added:**
  Syntax for non maximal implicit arguments in toplevel definitions using
  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
  to be consistent with the command :cmd:`Arguments (implicits)`.
  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
  by SimonBoulier).

Add changelog for non maximal implicit args
Add changelog for non maximal implicit args
