blob: 66139f76e100e7033a3d817f8d3fbdb8b3ffc1bc (
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).
|
