From f70a6e8d3e16fd472c8d09588b201da93f759db0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:57:26 +0100
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 100f37038..5413e760e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,11 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`**
+
+* Define non-expansive instance for `dom`. This, in particular, makes it
+  possible to `iRewrite` below `dom` (even if the `dom` appears in `âŒœ _ âŒ`).
+
 **Changes in `bi`:**
 
 * Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
-- 
GitLab