From 6e23e2d289439ffc7bdb6f245726c79ac2e0d323 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Dec 2021 17:51:53 +0100
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f64ab9dea..0dc1c0662 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,9 @@ lemma.
   [discardable fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction
   (`frac`). Lemmas affected by this have been renamed such that the "frac" in
   their name has been changed into "dfrac". (by Simon Friis Vindum)
+* Change `ufrac_auth` notation to not use curly braces, since these fractions do
+  not behave like regular fractions (and cannot be made `dfrac`).
+  Old: `●U{q} a`, `◯U{q} b`; new: `●U_q a`, `◯U_q b`.
 
 **Changes in `bi`:**
 
-- 
GitLab