diff --git a/CHANGELOG.md b/CHANGELOG.md index 3c06e152d1a04c0001da6f4b82726ad5fa1fc671..376da2cb466a417f2517ee3769c98a29c0e7e3a3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -96,7 +96,7 @@ Coq 8.11 is no longer supported in this version of Iris. `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal circumstances, this should be the only proofmode file you need to import. * Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`, - especially in the case of large goals and lemmas with many forall quantifiers + especially in the case of large goals and lemmas with many forall quantifiers. (by Armaël Guéneau) **Changes in `bi`:**