diff --git a/tex/iris.tex b/tex/iris.tex
index 0631f53daa8bd12331c635e23b74c7d226c1aae5..0a30cdda5a7e9d07391bbc13b8921eddddfd7519 100644
--- a/tex/iris.tex
+++ b/tex/iris.tex
@@ -14,7 +14,7 @@
 \input{setup}
 
 
-\title{\bfseries The Iris 3.7-dev Documentation}
+\title{\bfseries The Iris 4.0 Reference}
 \author{\url{http://plv.mpi-sws.org/iris/}}
 
 
@@ -24,7 +24,7 @@
 \thispagestyle{empty}
 \vfill
 \begin{abstract}
-This document describes formally the Iris program logic.
+This document formally describes the Iris program logic.
 Every result in this document has been fully verified in Coq.
 The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/iris/iris}.
 For further information, visit the Iris project website at \url{https://iris-project.org}.
diff --git a/tex/upload b/tex/upload
index 5874571c3252a550d75c5d53dd173855cd40044f..106922217a72ac7907e2011da7c3d0d70efe6d0e 100755
--- a/tex/upload
+++ b/tex/upload
@@ -3,5 +3,5 @@ set -e
 cd "$(dirname "$(readlink -e "$0")")"
 
 rub iris
-scp iris.pdf mpi-contact:plv.mpi-sws.org/iris/appendix-3.7.pdf
+scp iris.pdf mpi-contact:plv.mpi-sws.org/iris/appendix-4.0.pdf