blob: b6c87ed4b6c6c9ebaead85190e77ffaa328cc42a (
plain)
1
2
3
4
|
- **Added:** Syntax for specifying the variance of cumulative
polymorphic inductives (:ref:`cumulative`) instead of letting it be
inferred (`#12653 <https://github.com/coq/coq/pull/12653>`_, by
Gaëtan Gilbert).
|
