From 8288e56bbf737cde9eb2e36c3d634a5acbb04b83 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Mon, 12 Feb 2018 10:44:41 -0500 Subject: Add CHANGES entry for #1047 --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES b/CHANGES index cb4b966b0..1c4d8a194 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 -- cgit v1.2.3