From d0410021957cd5ad99e5a3ad054287ea928f192f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 19 Jun 2024 12:39:17 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 01cd77086..72a8c9eab 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,8 @@ lemma.
 
 * Remove the `*` specialization pattern. This pattern has been deprecated and a
   no-op since 2017. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/41.
+* Improve the error message of `iInv` in case the goal does not support
+  invariant opening.
 
 **Changes in `base_logic`:**
 
-- 
GitLab