aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
blob: d8ff1fec317335e29c9165cf74c93847c8c38782 (plain)
1
2
3
4
5
6
- **Added:**
  Syntax for non maximal implicit arguments in definitions and terms 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).