aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-14 14:23:29 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-14 14:23:29 +0100
commit41893cb647fbdce87b40acd5763e837370d61ece (patch)
tree6badf5503ba4f2c2fdd7e8ffa0b5e5469eba4279 /CHANGES
parentce7a851f21bd6e7c811bd3b7520019dabe609afc (diff)
parent8288e56bbf737cde9eb2e36c3d634a5acbb04b83 (diff)
Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 1084847d5..545925026 100644
--- a/CHANGES
+++ b/CHANGES
@@ -71,6 +71,8 @@ Universes
- Universe cumulativity for inductive types is now specified as a
variance for each polymorphic universe. See the reference manual for
more information.
+- Fix #5726: Notations that start with `Type` now support universe instances
+ with `@{u}`.
Checker