From fa81c7abea9423c20f5a129b6b81321ace677574 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Apr 2020 18:56:04 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f3bd2388a..b05d3f0bf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,12 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Better support for telescopes in the proof mode, i.e., all tactics should
   recognize and distribute telescopes now.
 * Remove namespace `N` from `is_lock`.
+* Make lemma `Excl_included` a bi-implication.
+* Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`,
+  and rename existing asymmetric lemmas (with a singleton on just the LHS):
+  + `singleton_includedN` → `singleton_includedN_l`.
+  + `singleton_included` → `singleton_included_l`.
+  + `singleton_included_exclusive_l` → `singleton_included_exclusive`
 
 **Changes in heap_lang:**
 
-- 
GitLab