From be5fe2c5f07dad765ed2d6b986696fe9172b4a64 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Feb 2018 19:47:04 +0100
Subject: [PATCH] Update changelog.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ff053daed..76bb4d769 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,11 @@ Changes in Coq:
 * 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 function space
   CMRA even for an infinite domain.
+* Rename proof mode type classes for laters:
+  - `IntoLaterN` → `MaybeIntoLaterN` (this one _may_ strip a later)
+  - `IntoLaterN'` → `IntoLaterN` (this one _should_ strip a later)
+  - `IntoLaterNEnv` → `MaybeIntoLaterNEnv`
+  - `IntoLaterNEnvs` → `MaybeIntoLaterNEnvs`
 
 ## Iris 3.1.0 (released 2017-12-19)
 
-- 
GitLab