From 4a9d93308bdd161d9dc0cc73d7ab35822fa1a7ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 00:50:52 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8629231f..80799303 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -61,6 +61,13 @@ API-breaking change is listed.
 - Rename instances `option_mbind_proper` → `option_bind_proper` and
   `option_mjoin_proper` → `option_join_proper` to be consistent with similar
   instances for sets and lists.
+- Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.
+  + Drop `DiagNone` class.
+  + Add `merge_proper` instance.
+  + Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+  + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
+    `partial_alter_merge_r`.
+  + Drop unused `merge_assoc'` instance.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
-- 
GitLab