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

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7747ffdae..3a5c93c59 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,8 @@ Coq 8.13 is no longer supported.
   `map_to_list`. (by Dorian Lesbre).
 - Make `persistently_True` a bi-entailment.
 - Make `BiLaterContractive` a class instead of a notation.
+- Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
+  classes `Typeclasses Opaque`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab