From e9543a9dc75e8da7642fad262e0c722d7f57636d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Jul 2021 15:17:56 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7c576cc6..df598d462 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,6 +59,7 @@ 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>`/`â†’`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab