aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTej Chajed2018-02-12 10:44:41 -0500
committerTej Chajed2018-02-13 09:34:19 -0500
commit8288e56bbf737cde9eb2e36c3d634a5acbb04b83 (patch)
tree15a0da5c0eb659f9d9475c4bc05be4ba15e810e4
parent52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff)
Add CHANGES entry for #1047
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index cb4b966b08..1c4d8a194c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,8 @@ Universes
module and library boundaries. Global universe names introduced in an
inductive / constant / Let declaration get qualified with the name of
the declaration.
+- Fix #5726: Notations that start with `Type` now support universe instances
+ with `@{u}`.
Checker