From dbfefce1ffd7fb962030bdabc4b8aabecbc91389 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2021 13:50:18 +0100
Subject: [PATCH] changelog
---
CHANGELOG.md | 2 ++
1 file changed, 2 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index ed7c5c3ba..49070971f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -210,6 +210,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
non-atomic weakest precondition creates a side-condition `Atomic ...`.
Before, this would fail with the unspecific error "iMod: cannot eliminate
modality (|={E1,E2}=> ...) in (WP ...)".
+* In `Ectx_step` and `step_atomic`, mark the parameters that are determined by
+ the goal as implicit.
**Changes in `heap_lang`:**
--
GitLab