From 7361c41234f09eea2457db8746134e2e66a4494a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 10:21:54 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d392df165..7747ffdae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,7 @@ Coq 8.13 is no longer supported.
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
   `map_to_list`. (by Dorian Lesbre).
 - Make `persistently_True` a bi-entailment.
+- Make `BiLaterContractive` a class instead of a notation.
 
 **Changes in `proofmode`:**
 
-- 
GitLab