From b78cbaa4c8f855f11b4f5d11f3cd008b9b8723ad Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 May 2021 11:19:17 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 768bf1001..975a03aa6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,10 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add support for destructing existentials with the intro pattern `[%x ...]`.
   (by Tej Chajed)
 
+**Changes in `bi`:**
+
+* Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`).
+
 **Changes in `base_logic`:**
 
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
-- 
GitLab