From 3db87055634a69577e9bb6d0fb388714896975e4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Nov 2019 13:27:20 +0100
Subject: [PATCH] add changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3db75fa7e..edf2268c4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris master
 
+**Changes in the theory of Iris itself:**
+
+* [#] Redefine invariants as "semantic invariants" so that they support
+  splitting and other forms of weakening.
+
 **Changes in Coq:**
 
 * A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
-- 
GitLab