From 9a6726437344c59084a3316791d656030d01d2f8 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 4 Jul 2018 08:04:24 +0200 Subject: [PATCH] changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 23cd9f4b3..2fe145928 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,8 @@ Changes in and extensions of the theory: * [#] The Löb rule is now a derived rule; it follows from later-intro, later being contractive and the fact that we can take fixpoints of contractive functions. +* [#] Add atomic updates and logically atomic triples, including tactic support. + See `heap_lang/lib/increment.v` for an example. Changes in Coq: -- GitLab