From ac62dc3e2b9f739a138280659f087c26022e9f9f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Mar 2019 10:19:22 +0100
Subject: [PATCH] Add CHANGELOG entry.

---
 CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3b99c4378..46ae8e6d0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -103,6 +103,9 @@ Changes in Coq:
 * The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
   sets, instead of just for cofinite sets. The versions with cofinite
   sets have been renamed to use the `_cofinite` suffix.
+* Remove locked value lambdas. The value scope notations `rec: f x := e` and
+  `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
+  smarter to no longer unfold lambdas/recs that occur behind definitions.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
-- 
GitLab