diff --git a/CHANGELOG.md b/CHANGELOG.md index bcbf9837333308d2cf4c3862da06fe91f7aab3d4..75866d8b84af4a60a0bf93022d96163337ec1e70 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`).