diff options
author | 2017-08-18 16:11:39 +0200 | |
---|---|---|
committer | 2017-08-18 16:11:39 +0200 | |
commit | 809cf4676c75d9a00f1fcd47e3c7d871a3dec83e (patch) | |
tree | 56a533d5ba4275ede0cc2adefdf84214bc8b65c3 | |
parent | 7221e3644b2503a8ba5e3c94eb703bd2bf0967b4 (diff) | |
parent | 2bb2877795ca1b6234dae05fe9b55e68abcd22ea (diff) |
Merge PR #983: Correct the option for cumulativity in CHANGES
-rw-r--r-- | CHANGES | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -156,7 +156,7 @@ Build Infrastructure Universes - Cumulative inductive types. see prefixes "Cumulative", "NonCumulative" - for inductive definitions and the option "Set Inductive Cumulativity" + for inductive definitions and the option "Set Polymorphic Inductive Cumulativity" in the reference manual. - New syntax `foo@{_}` to instantiate a polymorphic definition with anonymous universes (can also be used with `Type`). |