aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES12
1 files changed, 12 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index b5aaad725..8b3f9c9c3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -94,6 +94,18 @@ 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.
+
+XML Protocol
+
+- The `query` call has been modified, now it carries a mandatory
+ "route_id" integer parameter, that associated the result of such
+ query with its generated feedback.
+
Changes from V8.6beta1 to V8.6
==============================