adam@311: \documentclass[12pt]{report}
adam@311: \usepackage[]{inputenc}
adam@311: \usepackage[T1]{fontenc}
adam@468: \usepackage{lmodern}
adam@311: \usepackage{fullpage}
adam@311: \usepackage{coqdoc}
adam@311: \usepackage{amsmath,amssymb}
adam@311: \usepackage{url}
adam@311: \usepackage{makeidx,hyperref}
adam@311: 
adam@479: \newcommand{\naive}[0]{na\"ive}
adam@479: 
adam@311: \title{Certified Programming with Dependent Types}
adam@311: \author{Adam Chlipala}
adam@311: 
adam@311: \makeindex
adam@311: 
adam@311: \begin{document}
adam@311: 
adam@311: \maketitle
adam@311: 
adam@311: \thispagestyle{empty}
adam@311: \mbox{}\vfill
adam@311: \begin{center}
adam@311: 
adam@370: Copyright Adam Chlipala 2008-2012.
adam@311: 
adam@311: 
adam@311: This work is licensed under a
adam@311: Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@311: Unported License.
adam@311: The license text is available at:
adam@311: 
adam@311: \end{center}
adam@311: 
adam@311: \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
adam@311: 
adam@311: \phantomsection
adam@311: \tableofcontents
adam@311: 
adam@311: \include{Intro.v}
adam@311: \include{StackMachine.v}
adam@311: \include{InductiveTypes.v}
adam@311: \include{Predicates.v}
adam@311: \include{Coinductive.v}
adam@353: \include{Subset.v}
adam@350: \include{GeneralRec.v}
adam@311: \include{MoreDep.v}
adam@311: \include{DataStruct.v}
adam@311: \include{Equality.v}
adam@311: \include{Generic.v}
adam@311: \include{Universes.v}
adam@324: \include{LogicProg.v}
adam@311: \include{Match.v}
adam@311: \include{Reflection.v}
adam@311: \include{Large.v}
adam@381: \include{ProgLang.v}
adam@383: \include{Conclusion.v}
adam@311: 
adam@311: \clearpage
adam@311: \addcontentsline{toc}{chapter}{Bibliography}
adam@311: \bibliographystyle{plain}
adam@311: \bibliography{cpdt}
adam@311: 
adam@311: \clearpage
adam@311: \addcontentsline{toc}{chapter}{Index}
adam@311: \printindex
adam@311: 
adam@311: \end{document}