From 1c2ea26da11970fc44cb64133052c5071014a623 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Dec 2017 20:34:23 +0100
Subject: [PATCH] Add Changelog entry.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index baa924f03..2b37214d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -90,7 +90,9 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   + The version of big operations over lists was redefined so that it enjoys
     more definitional equalities.
 * Various improvements to `solve_ndisj`.
-* Improve handling of pure (non-state-dependent) reductions in heap_lang.
+* Some extensions/improvements of heap_lang:
+  - Improve handling of pure (non-state-dependent) reductions.
+  - Add fetch-and-add (`FAA`) operation.
 * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
-- 
GitLab