changelog

CHANGELOG.md

@@ -94,13 +94,15 @@ 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
+* 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
+* Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
   statement involves `let`.
+* Remove `string_to_ident`; use `string_to_ident_cps` instead which is in CPS
+  form and hence does not require awful hacks.
 
 **Changes in `base_logic`:**