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).
|