From 02b8536862f0a79d29ddd244772d32f9a9b6a792 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 27 Jun 2021 13:25:29 +0200
Subject: [PATCH] changelog for sum_inhabited_r fix

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bf57f09e..324d8cf3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -102,6 +102,7 @@ API-breaking change is listed.
 - Add lemmas for sets: `elem_of_weaken` and `not_elem_of_weaken`.
 - Rename `insert_delete` → `insert_delete_insert`; add new `insert_delete` that
   is consistent with `delete_insert`.
+- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
 
 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