From 365ae70bc897932b68f317eb184c30420aa808b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Jul 2021 08:58:41 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 019bda96a..98be6b415 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,7 +59,9 @@ Coq 8.11 is no longer supported in this version of Iris.
     As a consequence, `make_laterable_elim` got weaker: elimination now requires
     an except-0 modality (`make_laterable P -âˆ— â—‡ P`).
   - Add `iModIntro` support for `make_laterable`.
-* State `bi_mono_pred` using `â–¡`/`-âˆ—` instead of `<pers>`/`â†’`.
+* Improvements to `bi_mono_pred`:
+  - Use `â–¡`/`-âˆ—` instead of `<pers>`/`â†’`.
+  - Strengthen to ensure that functions for recursive calls are non-expansive.
 
 **Changes in `proofmode`:**
 
-- 
GitLab