diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6b056c827590fea750ad05505f39f9c2d4e52ac0..751a9cea7045889c8c1795f1e158e182936b2820 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 Changes in and extensions of the theory:
 
-* Add new modality: â–  ("plainly").
+* [Experimental feature] Add new modality: â–  ("plainly").
+* Define `uPred` as a quotient on monotone predicates `M -> SProp`.
 * Camera morphisms have to be homomorphisms, not just monotone functions.
 * Add a proof that `f` has a fixed point if `f^k` is contractive.
 * Constructions for least and greatest fixed points over monotone predicates