From 036358a32d245085866ed88e2edc96796c4d2993 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 19 May 2021 11:59:45 +0200 Subject: [PATCH] add credit in changelog --- CHANGELOG.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 217b29d55..cda1ecd30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,7 +13,7 @@ Coq 8.11 is no longer supported in this version of Iris. cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted `â—{#q} a` and `â—V{#q} a`. Lemmas affected by this have been renamed such that - the "frac" in their name has been changed into "dfrac". + the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum) * Generalize `namespace_map` to `reservation_map` which enhances `gmap positive A` with a notion of 'tokens' that enable allocating a particular name in the map. See [algebra.reservation_map](iris/algebra/reservation_map.v) for further @@ -32,8 +32,9 @@ Coq 8.11 is no longer supported in this version of Iris. * Add support for pure names `%H` in intro patterns. This is now natively supported whereas the previous experimental support required installing - https://gitlab.mpi-sws.org/iris/string-ident. + https://gitlab.mpi-sws.org/iris/string-ident. (by Tej Chajed) * Add support for destructing existentials with the intro pattern `[%x ...]`. + (by Tej Chajed) **Changes in `base_logic`:** -- GitLab