summaryrefslogtreecommitdiff
path: root/sec/intro.ltx
diff options
context:
space:
mode:
Diffstat (limited to 'sec/intro.ltx')
-rw-r--r--sec/intro.ltx2
1 files changed, 1 insertions, 1 deletions
diff --git a/sec/intro.ltx b/sec/intro.ltx
index 0a50ff4..f520bc4 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -24,7 +24,7 @@
\subsubsection*{Contributions}%
In this paper we:
-\begin{itemize}
+\begin{itemize}[nosep]
\item contrast different methods for encoding inductive types in
System~T (\cref{M-subsec:encoding-strategies});
\item give the syntax, typing rules and equational theory for