From e511ef1aff7d2103ad6189f3fa79c456c2a42392 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 1 Sep 2020 12:20:37 +0200 Subject: Changelog for variance syntax --- doc/changelog/02-specification-language/12653-cumul-syntax.rst | 9 +++++---- 1 file 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 `_, 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 ` + mode) (`#12653 `_, by Gaëtan + Gilbert). -- cgit v1.2.3