diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6fb5027e7a25492796c7f90e5f6c57346702ecb7..57a15c2fb11983e2e1ef060cbd282808c61f4499 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 12d02a6eabc183d7e284ea3d9f46cb51cfacafab..a45b2faa608514d630e45898851192030005e3fa 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