Commit 0202441f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent f02baee6
......@@ -184,6 +184,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
already at the top level).
* The `wp_` tactics now preserve the possibility of doing a fancy update when
the expression reduces to a value.
* Move `IntoVal`, `AsVal`, `Atomic`, `AsRecV`, and `PureExec` instances to their
own file [heap_lang.class_instances](iris_heap_lang/class_instances.v).
* Move `inv_head_step` tactic and `head_step` auto hints (now part of new hint
database `head_step`) to [heap_lang.tactics](iris_heap_lang/tactics.v).
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`).
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