From cb5834a89713c422d6fdab4644780150872d9d04 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 3 Jun 2019 18:00:42 +0200 Subject: [PATCH] Add Changelog entry. --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5ab682fcd..3b278c5c3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,8 @@ Changes in and extensions of the theory: describes the postcondition of each forked-off thread (instead of it being `True`). Additionally, there is a stronger variant of the adequacy theorem that allows to make use of the postconditions of the forked-off threads. +* The user-chosen functor used to instantiate the Iris logic now goes from + COFEs to Cameras (it was OFEs to Cameras). Changes in Coq: -- GitLab