diff --git a/formalism/formalism.tex b/formalism/formalism.tex
index c135b44..86ba211 100644
--- a/formalism/formalism.tex
+++ b/formalism/formalism.tex
@@ -3,7 +3,12 @@
 \input{preamble/preamble}
 \usepackage{subfiles}
 
+\title{Total Type Error Localization and Recovery with Holes}
+\date{}
+
 \begin{document}
+\maketitle
+
 \tableofcontents
 \newpage
 
diff --git a/formalism/preface.tex b/formalism/preface.tex
index 240586c..de7d3d2 100644
--- a/formalism/preface.tex
+++ b/formalism/preface.tex
@@ -23,8 +23,8 @@ \subsection{Organization}
   \item \cref{sec:typed} is similar, except that it employs the marking procedure in a roughly
     incremental fashion.
 
-  \item \cref{sec:constraint} gives the rules for constraint generation in relation to the type hole
-    inference work of Section 4.
+  \item \cref{sec:constraint} additionally gives the rules for constraint generation in relation to
+    the type hole inference work of Section 4.
 \end{itemize}
 %
 Note that each of the sections following \cref{sec:marked} build upon that same core language.