diff --git a/CHANGELOG.md b/CHANGELOG.md index 2ad4c79049417177c77fc533d1b1c5c03e95d29a..895664ff7e23e28762d6931d0a7594d0bc4d7ed9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,7 +12,7 @@ Coq development, but not every API-breaking change is listed. Changes marked updates. Weakestpre is defined inside the logic, and invariants and view shifts with masks are also coded up inside Iris. Adequacy of weakestpre is proven in the logic. -* Use OFEs instead of COFEs everywhere. COFEs are only used for solving the +* [#] Use OFEs instead of COFEs everywhere. COFEs are only used for solving the recursive domain equation. As a consequence, CMRAs no longer need a proof of completeness. (The old `cofeT` is provided by `algebra.deprecated`.)