From 11b32aa76f63525bb5bcf1b3171514f6f6830606 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 16:29:03 +0200
Subject: Univs/CHANGES: #4097 and annotations on notations

---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index dada2ed975..2533b01897 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,13 @@ Bugfixes
 - #4777: printing inefficiency with implicit arguments
 - #4752: CoqIDE crash on files not ended by ".v".
 - #4398: type_scope used consistently in "match goal".
+- #4097: more efficient occur-check in presence of primitive projections
+
+Universes:
+- Disallow silently dropping universe instances applied to variables
+  (forward compatible)
+- Allow explicit universe instances on notations, when they can apply
+  to the head reference of their expansion.
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3