From a78b08fa86384062e4f238492758bb53ff6984c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Jun 2021 15:51:33 +0200
Subject: [PATCH] fix typo in changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 07970642f..17fa7dac7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -52,7 +52,7 @@ Coq 8.11 is no longer supported in this version of Iris.
   explicit coercions in a few cases, in particular `WP v {{ Φ }}` must now be
   written `WP (of_val v) {{ Φ }}`.
 * Improve `make_laterable`:
-  - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable `.
+  - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable P`.
     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`.
-- 
GitLab