Merge PR #890: Global universe declarations

1 files changed, 10 insertions, 0 deletions

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