diff --git a/CHANGELOG.md b/CHANGELOG.md
index ff053daedffc41896b185471dd8d67870fe36640..76bb4d769858f1b55e2a0317d28316108a083454 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)