From 392a0447baa0fc26e71ac65ca7f58d5ad8239e4f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 23 Jul 2021 09:14:17 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 98be6b415..bb8a614dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,7 +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`.
-* Improvements to `bi_mono_pred`:
+* Improvements to `BiMonoPred`:
   - Use `â–¡`/`-âˆ—` instead of `<pers>`/`â†’`.
   - Strengthen to ensure that functions for recursive calls are non-expansive.
 
-- 
GitLab