From a8bc4651d974a4b25e3f026604ac62ae40af64b4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 Aug 2023 11:25:06 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 22fb3c621..9dfd0a3f2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,8 @@ Coq 8.13 is no longer supported.
   `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
   proofs. (by Ike Mulder)
 * Rename `singleton_mono` to `singleton_included_mono`.
+* Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
+  performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
 
 **Changes in `bi`:**
 
-- 
GitLab