From 3466b794c60c8c61eff4b0f80326c1111b839744 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Mar 2023 17:07:06 +0100
Subject: [PATCH] Add CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a25e051f7..185bb7e89 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,8 @@ Coq 8.13 is no longer supported.
   timeless hypotheses when proving an invariant (without an update).
 * Make `uPred.unseal` tactic more robust by using types to unfold the right
   BI projections.
+* Turn `internal_eq_entails` into a bi-implication.
+* Add lemmas to relate internal/external non-expansiveness and contractiveness.
 
 **Changes in `heap_lang`:**
 
-- 
GitLab