From 6c06af442da2ef8c8e5148775cb468711e7d33c5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 18:51:09 +0100
Subject: [PATCH] update CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 72efeb033..fa2dfe454 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Renaming and moving things around: uPred and the rest of the base logic are
   in `base_logic`, while `program_logic` is for everything involving the
   general Iris notion of a language.
+* [#] Slightly weaker notion of atomicity: an expression is atomic if it reduces
+  in one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation
   is ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.
   (The old notations are provided in `base_logic.deprecated`.)
-- 
GitLab