Update Changelog.

00c38f1f · Jacques-Henri Jourdan · d5390996 · 00c38f1f
Commit 00c38f1f authored Feb 20, 2018 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

CHANGELOG.md CHANGELOG.md +3 -0

No files found.
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,9 @@ Changes in and extensions of the theory:
 Changes in Coq:

 * Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
+* The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead
+  of in `Prop` using `exists`. This makes it possible to define the functionnal
+  CMRA even for an infinite domain.

 ## Iris 3.1.0 (released 2017-12-19)