diff --git a/CHANGELOG.md b/CHANGELOG.md
index fcb01da5bd8841b1d20b64371a3d2ac20e9c5b07..4adcf9a394f767196124e3d939110f407a47c466 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,9 @@ lemma.
   `Forall2` (for example, for trees with finite branching).
 * Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
   implication.
+* Change `of_envs` such that when the persistent context is empty, the
+  persistence modality no longer appears at all. This is a step towards using
+  the proofmode in logics without a persistence modality.
 
 **Changes in `base_logic`:**