From f7840f2a0ab1577b356fef90ff1bdcf3882551b0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Jun 2022 22:10:46 -0400
Subject: [PATCH] changelog

---
 CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fcb01da5b..4adcf9a39 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`:**
 
-- 
GitLab