From 458a3fa8df7216065573c08b95ddf5999373956f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 08:21:00 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 81e65e0e..712c4b8a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,7 +6,8 @@ API-breaking change is listed.
 Coq 8.11 is no longer supported.
 
 - Make sure that `gset` and `mapset` do not bump the universe.
-- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock Systems)
+- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock
+  Systems)
 - Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
   now inferred automatically. To make this possible, getting the domain of a
   `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
@@ -14,6 +15,9 @@ Coq 8.11 is no longer supported.
   When combining `dom` with `≡`, this can run into an old issue (due to a Coq
   issue, `Equiv` does not the desired `Hint Mode !`), which can make it
   necessary to annotate the set type at the `≡` via `≡@{D}`.
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
+  `nclose_eq`. These unsealing lemmas are internal, so in principle you should
+  not rely on them.
 
 ## std++ 1.7.0 (2022-01-22)
 
-- 
GitLab