From 245fd1f0e8bea7b78b2392dc5a17cee3ff74c395 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 11:33:13 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 897bc5fe1..3054df8ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
   This construct is *not* declared as an instance to avoid TC search divergence.
   (by Hai Dang, BedRock Systems)
+* Improve notation printing around `WP`, Texan triples, and logically atomic triples.
+* Slight change to the `AACC` notation for atomic accessors (which is usually
+  only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab