From 725a629741ed2670564f5ade0bf15a4171cb7a0e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Jul 2018 13:03:59 +0200
Subject: [PATCH] expand changelog
---
CHANGELOG.md | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 189e74895..090c811a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,12 +23,17 @@ Changes in and extensions of the theory:
Changes in Coq:
-* An all-new generalized proofmode that abstracts away from Iris! The proofmode
- can now be used with logics derived from Iris (like iGPS), with
- non-step-indexed logics and even with non-affine (i.e., linear) logics. See
- <http://iris-project.org/mosel/> for the corresponding paper.
- Developments instantiating the proofmode typeclasses may need significant
- changes. For developments just using the proofmode tactics, porting should
+* An all-new generalized proof mode that abstracts away from Iris! See
+ <http://iris-project.org/mosel/> for the corresponding paper. Major new
+ features:
+ - The proof mode can now be used with logics derived from Iris (like iGPS),
+ with non-step-indexed logics and even with non-affine (i.e., linear) logics.
+ - `iModIntro` is more flexible and more powerful, it now also subsumes
+ `iNext` and `iAlways`.
+ - General infrastructure for deriving a logic for monotone predicates over
+ an existing logic (see the paper for more details).
+ Developments instantiating the proof mode typeclasses may need significant
+ changes. For developments just using the proof mode tactics, porting should
not be too much effort. Notable things to port are:
- All the BI laws moved from the `uPred` module to the `bi` module. For
example, `uPred.later_equivI` became `bi.later_equivI`.
--
GitLab