diff --git a/CHANGELOG.md b/CHANGELOG.md index 499d197afa77ef2dabe8ffd5100829d2b539067b..2226209da8a6f38d943abe892558744af9d2089e 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`:**