From 42aa1a10cb6d707c12e6b5be2d4175b114350d1e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Jun 2021 13:28:27 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 607fdf3d9..0ee3339d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,11 @@ Coq 8.11 is no longer supported in this version of Iris.
   `big_sep{L,L2,M,M2,S}_intro`, and `big_orL_lookup` → `big_orL_intro`.
 * Rename `bupd_forall` to `bupd_plain_forall`, and add
   `{bupd,fupd}_{and,or,forall,exist}`.
+* Decouple `Wp` and `Twp` typeclasses from the `program_logic.language`
+  interface. The typeclasses are now parameterized over an expression and a
+  value type, instead of a language. This requires extra type annotations or
+  explicit coercions in a few cases, in particular `WP v {{ Φ }}` must now be
+  written `WP (of_val v) {{ Φ }}`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab