diff --git a/CHANGELOG.md b/CHANGELOG.md index 7747ffdaedb30b08d970e91af3b2dc9cc4bfbb9b..3a5c93c594d515a9ab83d42e5010169235a50fdd 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`:**