diff --git a/CHANGELOG.md b/CHANGELOG.md index 6fc46545f0246248e972aac2be342743d7785911..a1dd5effebfba19d070a9803f1297c648208fe1c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -99,6 +99,9 @@ Coq 8.11 is no longer supported in this version of Iris. * Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`, especially in the case of large goals and lemmas with many forall quantifiers. (by Armaël Guéneau) +* Improve performance of the `iDestruct` tactic, by using user-provided names + more eagerly in order to avoid later calls to `iRename`. + (by Armaël Guéneau) **Changes in `bi`:**