From 9fae57da04fdf112e969e634676c42ccf6f73046 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 30 Dec 2021 15:18:08 +0100
Subject: [PATCH] Update documentation & changelog

---
 CHANGELOG.md                | 5 +++++
 iris_heap_lang/metatheory.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6fb5027e7..57a15c2fb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,11 @@ lemma.
   assumptions to remain compatible, and code that instantiates the BI interface
   needs to provide instances for the new classes.
 
+**Changes in `heap_lang`:**
+
+* The `is_closed_expr` predicate is formulated in terms of a
+  set of binders (as opposed to a list of binders).
+
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.
diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index 12d02a6ea..a45b2faa6 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 (* This file contains some metatheory about the heap_lang language,
   which is not needed for verifying programs. *)
 
-(* Lifting `Insert` on strings to binders. *)
+(* Adding a binder to a set of identifiers. *)
 Local Definition set_binder_insert (x : binder) (X : stringset) : stringset :=
   match x with
   | BAnon => X
-- 
GitLab