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 b5aaad725e..deca62f921 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


From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 11:41:40 +0200
Subject: [ide] Add route_id parameter to query call.

This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.

This change is necessary in order to fix bug ####.
---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b5aaad725e..c6228e55ee 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".
 
+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
 ==============================
 
-- 
cgit v1.2.3