From e28d3a488c81c6dc59aa8f53d98a95ee93a84d37 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 23 May 2017 23:28:39 +0200 Subject: Document cumulativity for inductive types --- CHANGES | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index b5aaad725..deca62f92 100644 --- a/CHANGES +++ b/CHANGES @@ -94,6 +94,12 @@ Build Infrastructure access to the same .cmi files. In short, use "make -j && make -j byte" instead of "make -j world byte". +Universes + +- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative" + for inductive definitions and the option "Set Inductive Cumulativity" + in the reference manual. + Changes from V8.6beta1 to V8.6 ============================== -- cgit v1.2.3