From 4ce839b82e0ed04dcda37aa09b002177f0b5b2eb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 16:44:14 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 04eb4aeee..07970642f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,6 +51,11 @@ Coq 8.11 is no longer supported in this version of Iris.
   value type, instead of a language. This requires extra type annotations or
   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 `.
+    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`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab