diff --git a/CHANGELOG.md b/CHANGELOG.md
index 37dad38922701f65d6fe10d44cfd9a6a375e3bdd..ca6541a891edc1732467233f051a7d1564b14c10 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,10 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
     tactics now no longer work when the universal quantifier or modality is
     behind a type class opaque definition.  Furthermore, this can change the
     name of anonymous identifiers introduced with the "%" pattern.
+* Make `ofe_fun` dependently typed, subsuming `iprod`.  The latter got removed.
+* Generalize `saved_prop` to let the user choose the location of the type-level
+  later.  Rename the general form to `saved_anything`.  Provide `saved_prop` and
+  `saved_pred` as special cases.
 * Define the generic `fill` operation of the `ectxi_language` construct in terms
   of a left fold instead of a right fold. This gives rise to more definitional
   equalities.