From ae859c84ed6d8f0f0947e3a9502be8c6f93c9754 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Jan 2020 20:34:30 +0100
Subject: [PATCH] CHANGELOG entry.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 712efda11..4d1b50809 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)
 
-- 
GitLab