CHANGELOG.

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`:**