diff --git a/CHANGELOG.md b/CHANGELOG.md
index ed7c5c3bafcb1bc33715e36521649b1330c5b799..49070971fb2f02fae5c3f50f18a43fb3dc556c2c 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`:**