Merge remote-tracking branch 'upstream/trunk' into trunk

1 files changed, 12 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b5aaad725e..8b3f9c9c34 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
 ==============================