From 816b3323cde3060d1f57161a9a2b75e90fd16062 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 May 2023 20:19:04 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 15f6f2ea9..7bc213c23 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -90,6 +90,8 @@ Coq 8.13 is no longer supported.
 - 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"`.
+  This can break some proofs that did `iIntros "?"` on a goal of the shape
+  `let ... in P âŠ¢ Q`.
 - Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
   statement involves `let`.
 
-- 
GitLab