diff --git a/CHANGELOG.md b/CHANGELOG.md
index 712efda11c973c60d43507ca8cda39c5bc9f36a8..4d1b50809929b55129e6e7dfde89b916143f28d6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Removed `Core` type class for defining the total core; it is now always
   defined in terms of the partial core. The only user of this type class was the
   STS RA.
+* Added the type `siProp` of "plain" step-indexed propositions, together with
+  basic proofmode support.
 
 ## Iris 3.2.0 (released 2019-08-29)