From fcdbf9b5cea9943171ba5e2fd17c653899d71255 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Dec 2020 14:08:41 +0100
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4fe9f93ba..cced70777 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -143,6 +143,20 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   initial heap.
 * Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler
   `mapsto_ne` that does not require reasoning about fractions.
+* Generalize the `gen_heap` library to discardable fractions.
+  + The `mapsto` connective now takes a `dfrac` rather than a `frac` (i.e.,
+    positive rational number `Qp`).
+  + The notation `l ↦{ dq } v` is generalized to discardable fractions
+    `dq : dfrac`.
+  + The new notation `l ↦{# q} v` is used for a concrete fraction `q : frac`
+    (e.g., to enable writing `l ↦{# 1/2} v`).
+  + The new notation `l ↦□ v` is used for the discarded fraction.
+  + The lemma `mapsto_persist : l ↦{dq} v ==∗ l ↦□ v` has been added.
+  + See the changes to HeapLang for an indication on how to adapt your language.
+  + See the changes to iris-examples for an indication on how to adapt your
+    development. In particular, instead of `∃ q, l ↦{q} v` you likely want to
+    use `l ↦□ v`, which has the advantage of being persistent (rather than just
+    duplicable).
 
 **Changes in `program_logic`:**
 
@@ -153,6 +167,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   avoid TC search attempting to apply this instance all the time.
 * Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by
   making the lemma bidirectional.
+* Generalize HeapLang's `mapsto` (`↦`) and `array` (`↦∗`) connectives to
+  discardable fractions. See the CHANGELOG entry in the category `base_logic`
+  for more information.
+* Generalize HeapLang's atomic heap to discardable fractions.
 
 **Changes in `heap_lang`:**
 
-- 
GitLab