diff --git a/formalism/constraint.tex b/formalism/constraint.tex
index 8fb4d5b..0a0d887 100644
--- a/formalism/constraint.tex
+++ b/formalism/constraint.tex
@@ -7,10 +7,9 @@
 \input{symbols/constraint}
 
 \section{Constraint generation}
-\label{constraint}
-
-A list of constraint generating bidirectional typing rules under the marked lambda calculus for type
-hole inference (see Section 4). \\
+\label{sec:constraint}
+Here, we give the list of constraint-generating bidirectional typing rules under the marked lambda
+calculus for type hole inference, described in Section 4 of the paper.
 
 \judgbox{\ensuremath{\matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched arrow type $\TArrow{\TMV_1}{\TMV_2}$ and generates constraints $C$
 \begin{mathpar}
diff --git a/formalism/marked.tex b/formalism/marked.tex
index 6f56181..bd1cd87 100644
--- a/formalism/marked.tex
+++ b/formalism/marked.tex
@@ -10,8 +10,7 @@ \section{Marked lambda calculus}
 
 The \emph{marked lambda calculus} is a judgmental framework for bidirectional type error
 localization and recovery. Here, we demonstrate it on a gradually typed lambda calculus with
-numbers, booleans, and product types. Typed holes (written $\EEHole$) are included to model
-incomplete editor states \`a la Hazelnut but are not essential.
+numbers, booleans, and product types, as described in Section 2.1 of the paper.
 
 \begin{mechanization}
   \item core.agda
diff --git a/formalism/patterned.tex b/formalism/patterned.tex
index 7d1e7ad..e305eab 100644
--- a/formalism/patterned.tex
+++ b/formalism/patterned.tex
@@ -8,6 +8,8 @@
 
 \section{Extension: patterned let expressions}
 \label{sec:patterned}
+In this section, we describe an extension of the marked lambda calculus for destructuring let
+expressions, as described in Section 2.3 of the paper.
 
 \nomechanization{}
 
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
index 30ecdab..92d914a 100644
--- a/formalism/polymorphism.tex
+++ b/formalism/polymorphism.tex
@@ -9,22 +9,12 @@
 \section{Extension: System F-style polymorphism}
 \label{sec:polymorphism}
 In this section, we describe an extension of the marked lambda calculus for System F-style
-parametric polymorphism.
-
-Chiefly, the introduction of type variables and the possibility of free ones requires the
-distinction between unmarked and marked types. These are each governed by well-formedness judgments
-(alongside extensions of the original consistency, etc. judgments) and linked by a marking
-operation.
+parametric polymorphism, as sketched out in Section 2.4 of the paper.
 
 \nomechanization{}
 
 \subsection{Syntax}
 \label{sec:polymorphism-syntax}
-The syntax of unmarked types is exactly that of the original types alongside additional forms for
-forall types and type variables. In marked types, we additionally have free type variables.
-Within unmarked expressions, there may be type abstractions and type applications. In marked
-expressions, marks corresponding to those of ordinary lambda abstractions are present.
-
 \[\begin{array}{rrcl}
   \TMName  & \TMV  & \Coloneqq & \cdots \mid \TForall{\TVarMV}{\TMV} \mid \TVarMV \\
   \MTMName & \MTMV & \Coloneqq & \cdots
@@ -38,10 +28,6 @@ \subsection{Syntax}
 
 \subsection{Unmarked types}
 \label{sec:polymorphism-unmarked-types}
-Type consistency is now parametrized by the type variable context $\tvarCtx$. Here (and similarly
-the extension of other judgments), we omit the rules for the old syntactic constructs, which may be
-straightforwardly derived from the original rules. \\
-
 \judgbox{\ensuremath{\tvarCtxConsistentU{\tvarCtx}{\TMV_1}{\TMV_2}}} $\TMV_1$ and $\TMV_2$ are consistent
 %
 \begin{mathpar}
diff --git a/formalism/preface.tex b/formalism/preface.tex
index a7e9ddb..240586c 100644
--- a/formalism/preface.tex
+++ b/formalism/preface.tex
@@ -22,6 +22,9 @@ \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.
 \end{itemize}
 %
 Note that each of the sections following \cref{sec:marked} build upon that same core language.
diff --git a/formalism/typed.tex b/formalism/typed.tex
index bf59932..a2ef3de 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -12,7 +12,8 @@ \section{Typed hazelnut}
 We now give a description of a \emph{typed} version of the Hazelnut action calculus that
 incorporates the marked lambda calculus to solve the problem of non-local hole fixes. Here, unlike
 in the integration of the untyped version and the marked lambda calculus given in
-\cref{sec:untyped}, remarking is performed only when necessary instead of after every action.
+\cref{sec:untyped}, remarking is performed only when necessary instead of after every action. This
+system is sketched out in Section 3.2 of the paper.
 
 \nomechanization{}
 
diff --git a/formalism/untyped.tex b/formalism/untyped.tex
index 541203d..d7d9739 100644
--- a/formalism/untyped.tex
+++ b/formalism/untyped.tex
@@ -9,12 +9,7 @@ \section{Untyped hazelnut}
 \label{sec:untyped}
 In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be
 layered with the marked lambda calculus to yield a structure editing calculus that supports
-non-local hole fixes.
-
-In comparison with the original calculus, this untyped version is not concerned at all with typing
-but only the manipulation of syntax. As such, the action judgments are simplified considerably; in
-particular, they are no longer bidirectional. The same core metatheorems, except sensibility which
-is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}).
+non-local hole fixes. This is described in Section 3.2 of the paper.
 
 \begin{mechanization}
   \item hazelnut.agda