diff options
| author | Gaëtan Gilbert | 2020-09-01 12:20:37 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:21:16 +0100 |
| commit | e511ef1aff7d2103ad6189f3fa79c456c2a42392 (patch) | |
| tree | 5f4133fc0bf6e18f27e7a87c9b8d972b3fead21b | |
| parent | ed6bee77f09200797a482c648b17ef5fa768aeac (diff) | |
Changelog for variance syntax
| -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). |