From fd8ca35a278fef4120d0bc455b19aaf6dd4e5fe5 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 4 Sep 2024 12:44:24 +0200
Subject: [PATCH] paper: add new coq files to appendix

---
 paper/appendix.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/paper/appendix.tex b/paper/appendix.tex
index 9826823..aa2c75b 100644
--- a/paper/appendix.tex
+++ b/paper/appendix.tex
@@ -20,11 +20,23 @@ This document lists the Coq-Sourcecode from commit
 \label{coq:equiv}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
 
+\subsection{subtype.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subtype.v}
+
 \subsection{typing.v}
 \label{coq:typing}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
 
+\subsection{morph.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/morph.v}
+
 \subsection{smallstep.v}
 \label{coq:smallstep}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
 
+\subsection{soundness.v}
+\label{coq:smallstep}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/soundness.v}
+