blob: ba97f7c7961f8b59217c619c0f9d62686b1f3d65 (
plain)
1
2
3
4
5
|
- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now
support syntax `Inductive foo@{=i +j *k l}` to specify variance
information for their universes (in :ref:`Cumulative <cumulative>`
mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan
Gilbert).
|
