doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst


1
2
3
4
5
6
7
8

- **Added:**
  :cmd:`Arguments <Arguments (implicits)>` now supports setting
  implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`.
  (`#11098 <https://github.com/coq/coq/pull/11098>`_,
  by Hugo Herbelin, fixes `#4696
  <https://github.com/coq/coq/pull/4696>`_, `#5173
  <https://github.com/coq/coq/pull/5173>`_, `#9098
  <https://github.com/coq/coq/pull/9098>`_.).