From 754ee8b236573c24cca3a34cbfcf94bed6059aa4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Mar 2021 18:35:51 +0100
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3ac18c6dd..89a56d939 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,11 +25,12 @@ lemma.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 
-**Changes in `proof_mode`:**
+**Changes in `proofmode`:**
 
 * Add support for pure names `%H` in intro patterns. This is now natively
   supported whereas the previous experimental support required installing
   https://gitlab.mpi-sws.org/iris/string-ident.
+* Add support for destructing existentials with the intro pattern `[% ...]`.
 
 **Changes in `base_logic`:**
 
-- 
GitLab