From 026ef1abf4a112da16d3f6978aae8e8e354ea4f2 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 25 Jul 2023 15:49:38 +0200
Subject: [PATCH] CHANGELOG for #2030: fix large indices

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 092d73a881..1da4157a62 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -733,6 +733,13 @@ Non-backwards compatible changes
 * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
   the `--without-K` flag now use the `--cubical-compatible` flag instead.
 
+* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4,
+  universe levels have been increased in the following definitions:
+  - `Data.Star.Decoration.DecoratedWith`
+  - `Data.Star.Pointer.Pointer`
+  - `Reflection.AnnotatedAST.Typeₐ`
+  - `Reflection.AnnotatedAST.AnnotationFun`
+
 * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base`
   have been made implicit.