diff options
| -rw-r--r-- | doc/changelog/02-specification-language/12653-cumul-syntax.rst | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst index b6c87ed4b6..ba97f7c796 100644 --- a/doc/changelog/02-specification-language/12653-cumul-syntax.rst +++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst @@ -1,4 +1,5 @@ -- **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). +- **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). |