\documentclass[a4paper]{article}

\usepackage{import}
\import{}{preamble}
% The mfpic stuff is in its own preamble file, as mfpic goes wrong
% if we import this into the generated .mp file
\import{}{preamble_mfpic}

\begin{document}

\import{}{definitions}

\title{Camp Patch Theory}
\author{Ian Lynagh}
\maketitle

% We can't use % as a comment character in files that go through coqdoc,
% as it uses that as the latex escape character. Sigh. So we use #
% instead.
\catcode`\#14

\tableofcontents
\import{}{overview}
\import{tex/}{notation}
\import{tex/}{unnamed_patches}
\import{tex/}{unnamed_patch_sequences}
\import{}{sensible_unnamed_patch_sequences}
\import{tex/}{names}
\import{tex/}{named_patches}
\import{}{patch_merge}
\import{tex/}{patch_universes}
\import{tex/}{merging}
\import{tex/}{contexted_patches}
\import{tex/}{catches_definition}
\import{tex/}{catches}
\import{tex/}{catches_commute_consistent}
\import{tex/}{catches_commute_consistent_1_1}
\import{tex/}{catches_commute_consistent_1_2}
\import{tex/}{catches_commute_consistent_1_3}
\import{tex/}{catches_commute_consistent_1_4}
\import{tex/}{catches_commute_consistent_1_5}
\import{tex/}{catches_commute_consistent_1_6}
\import{tex/}{catches_commute_consistent_1_7}
\import{tex/}{catches_commute_consistent_1_8}
\import{tex/}{catch_patch_universe}
\import{tex/}{hunks}
\appendix
\import{}{catch_more_bits}
\import{}{named_patch_motivation}

\closegraphsfile
\end{document}

