diff --git a/CHANGELOG.md b/CHANGELOG.md index 100f370387082e79beca24b74bc4358c1fb8bdd1..5413e760ec0dcde2da508038d671da3f663b2700 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`,