diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83c26d5dd4617e780143600e3b59f2a4eba4310f..15f6f2ea997c9a5fc98c7b466d18305ebc96747c 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`:**