--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/latex/cpdt.tex	Mon Aug 29 15:31:06 2011 -0400
@@ -0,0 +1,69 @@
+\documentclass[12pt]{report}
+\usepackage[]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\usepackage{makeidx,hyperref}
+
+\title{Certified Programming with Dependent Types}
+\author{Adam Chlipala}
+
+\makeindex
+
+\begin{document}
+
+\maketitle
+
+\thispagestyle{empty}
+\mbox{}\vfill
+\begin{center}
+
+Copyright Adam Chlipala 2008-2011.
+
+
+This work is licensed under a
+Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+Unported License.
+The license text is available at:
+
+\end{center}
+
+\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
+
+\phantomsection
+\tableofcontents
+
+\include{Intro.v}
+\include{StackMachine.v}
+\include{InductiveTypes.v}
+\include{Predicates.v}
+\include{Coinductive.v}
+\include{Subset.v}
+\include{MoreDep.v}
+\include{DataStruct.v}
+\include{Equality.v}
+\include{Generic.v}
+\include{Universes.v}
+\include{Match.v}
+\include{Reflection.v}
+\include{Large.v}
+\include{Firstorder.v}
+\include{DeBruijn.v}
+\include{Hoas.v}
+\include{Interps.v}
+\include{Extensional.v}
+\include{Intensional.v}
+\include{OpSem.v}
+
+\clearpage
+\addcontentsline{toc}{chapter}{Bibliography}
+\bibliographystyle{plain}
+\bibliography{cpdt}
+
+\clearpage
+\addcontentsline{toc}{chapter}{Index}
+\printindex
+
+\end{document}