From a3534b51226f93379b1ec75367f33ae68b81a5d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 10:07:46 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ec01cb19b..0b1d6aff1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,13 @@ lemma.
 
 ## Iris master
 
+**General changes:**
+
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This particularly
+  affects `envs_entails_eq`, which is commonly used in the definition of
+  custom proof mode tactics. All other unsealing lemmas should be internal, so
+  in principle you should not rely on them.
+
 **Changes in `bi`:**
 
 * Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
-- 
GitLab