diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca6541a891edc1732467233f051a7d1564b14c10..baa924f03902faad3331dd42951266189d6c5043 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 Changes in and extensions of the theory:
 
-* [#] Add new modality: â–  ("plainly").
+* Add new modality: â–  ("plainly").
 * Camera morphisms have to be homomorphisms, not just monotone functions.
 * Add a proof that `f` has a fixed point if `f^k` is contractive.
 * Constructions for least and greatest fixed points over monotone predicates
diff --git a/docs/iris.tex b/docs/iris.tex
index 83d56c6d7aa6b9e1a67b75449110abedc0082149..dfe6a1dbc75fb3121ae453c90d5fc7b91579f9e3 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -16,7 +16,7 @@
 \input{setup}
 
 
-\title{\bfseries The Iris 3.0 Documentation}
+\title{\bfseries The Iris 3.1 Documentation}
 \author{\url{http://plv.mpi-sws.org/iris/}}