From 17b620f8bdf47a744d24513dcaef720d9160d443 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:15:25 +0100
Subject: Update CHANGES

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

diff --git a/CHANGES b/CHANGES
index 4c83b7c19d..da346c04db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,10 +22,20 @@ Tactics
   contain proofs.
 
 Vernacular Commands
+
 - The deprecated Coercion Local, Open Local Scope, Notation Local syntax
   was removed. Use Local as a prefix instead.
 
+Universes
+
+- Qualified naming of global universes now works like other namespaced
+  objects (e.g. constants), with a separate namespace, inside and across
+  module and library boundaries. Global universe names introduced in an
+  inductive / constant / Let declaration get qualified with the name of
+  the declaration.
+
 Checker
+
 - The checker now accepts filenames in addition to logical paths.
 
 Changes from 8.7+beta2 to 8.7.0
-- 
cgit v1.2.3