From 25c754ccea78526840ed921d0ebea7ab44f1fa23 Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Fri, 21 Apr 2017 15:09:16 +0200
Subject: [PATCH] Include typing rules into the global document

---
 combined/main.tex      |  2 +-
 typing/type-system.tex | 17 -----------------
 2 files changed, 1 insertion(+), 18 deletions(-)

diff --git a/combined/main.tex b/combined/main.tex
index 5091d90..3635b98 100644
--- a/combined/main.tex
+++ b/combined/main.tex
@@ -26,7 +26,7 @@ We also present a compilation from nix to nix-light.
 
 \section{typing}
 
-\todo{Finish and include the typing rules}
+\input{typing/type-system.tex}
 
 \todos{}
 
diff --git a/typing/type-system.tex b/typing/type-system.tex
index 7182a5e..6b0cfae 100644
--- a/typing/type-system.tex
+++ b/typing/type-system.tex
@@ -1,16 +1,3 @@
-\input{common/header}
-
-\title{A type system for nix}
-
-\begin{document}
-
-\maketitle{}
-
-\section{Types}
-
-\include{grammar/types}
-
-\section{Typing rules}
 \subsection{$\lambda\&$-calculus}
 \begin{mathpar}
   \inferrule{ }{\Gamma; x:\tau \vdash x:\tau}(Var)
@@ -69,7 +56,3 @@
 
 \subsection{Other builtin operators}
 \todo{add rules for operators}
-
-\todos
-
-\end{document}