From c3cb95faab1a3dbf46433e2bcfb9cabe520f3dd4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 May 2023 21:17:02 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83c26d5dd..15f6f2ea9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -87,6 +87,11 @@ Coq 8.13 is no longer supported.
   `CombineSepGives` typeclass. The 'gives' clause is still experimental;
   in future versions of Iris it will combine `own` connectives based on the
   validity rules for cameras.
+- Make sure that `iStartProof` fails with a proper error message on goals with
+  `let`. These `let`s should either be `simpl`ed or introduced into the Coq
+  context using `intros x`, `iIntros (x)`, or `iIntros "%x"`.
+- Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
+  statement involves `let`.
 
 **Changes in `base_logic`:**
 
-- 
GitLab