diff --git a/CHANGELOG.md b/CHANGELOG.md index f64ab9dea17745aa54dc4aee4ccbe4c2db1cba45..0dc1c0662689c222dbc3d8016f7a58afdae0e1ad 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`:**