From 9ae97e032af591a498cda62c8aea3a75d400aeae Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Sat, 9 Sep 2023 16:43:07 +0000
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 499d197af..2226209da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -50,6 +50,9 @@ Coq 8.13 is no longer supported.
 * Rename `singleton_mono` to `singleton_included_mono`.
 * Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
   performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
+* Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
+  monotonicity with respect to an arbitrary preorder relation: the extension order
+  of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
 
 **Changes in `bi`:**
 
-- 
GitLab