From 0202441f31569844ca2f7f63a5f4d1fd52eea513 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 4 Jan 2021 23:02:43 +0100 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index bcbf98373..75866d8b8 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`). -- GitLab