Commit 9fae57da authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers
Browse files

Update documentation & changelog

parent bc626812
......@@ -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.
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment