From 00c38f1f1396260f78776f4859662bdb3a1d2196 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 20 Feb 2018 16:54:25 +0100
Subject: [PATCH] Update Changelog.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index aff5d2f3f..ed9e0739f 100644
--- 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)
 
-- 
GitLab