blob: 11d7218ed073cd3c94c865ff6f562c028c9116a4 (
plain)
1
2
3
4
5
6
|
- **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).
|
