From 5a0cf609be98b051a2cb92a96b6195f840358d5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org> Date: Sun, 19 Sep 2021 23:00:24 +0200 Subject: [PATCH] add CHANGELOG entry --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6fc46545f..a1dd5effe 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`:** -- GitLab