Update documentation & changelog

CHANGELOG.md

@@ -32,6 +32,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.

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