annotate latex/cpdt.tex @ 546:306539f29eea

Make specially licensed versions of lib files for cpdtlib.tgz. This adds an ocaml tool and calls to it in the Makefile.
author Arthur Peters <amp@singingwizard.org>
date Thu, 12 May 2016 18:09:36 -0500
parents d65e9c1c9041
children dcb240e19167
rev   line source
adam@311 1 \documentclass[12pt]{report}
adam@311 2 \usepackage[]{inputenc}
adam@311 3 \usepackage[T1]{fontenc}
adam@468 4 \usepackage{lmodern}
adam@311 5 \usepackage{fullpage}
adam@311 6 \usepackage{coqdoc}
adam@311 7 \usepackage{amsmath,amssymb}
adam@311 8 \usepackage{url}
adam@311 9 \usepackage{makeidx,hyperref}
adam@311 10
adam@479 11 \newcommand{\naive}[0]{na\"ive}
adam@479 12
adam@311 13 \title{Certified Programming with Dependent Types}
adam@311 14 \author{Adam Chlipala}
adam@311 15
adam@311 16 \makeindex
adam@311 17
adam@311 18 \begin{document}
adam@311 19
adam@311 20 \maketitle
adam@311 21
adam@532 22 A print version of this book is available from the MIT Press. For more information, see the book's home page:
adam@532 23
adam@532 24 \begin{center} \url{http://adam.chlipala.net/cpdt/} \end{center}
adam@532 25
adam@311 26 \thispagestyle{empty}
adam@311 27 \mbox{}\vfill
adam@311 28 \begin{center}
adam@311 29
adam@536 30 Copyright Adam Chlipala 2008-2013, 2015.
adam@311 31
adam@311 32
adam@311 33 This work is licensed under a
adam@311 34 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@311 35 Unported License.
adam@311 36 The license text is available at:
adam@311 37
adam@311 38 \end{center}
adam@311 39
adam@311 40 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
adam@311 41
adam@311 42 \phantomsection
adam@311 43 \tableofcontents
adam@311 44
adam@311 45 \include{Intro.v}
adam@311 46 \include{StackMachine.v}
adam@311 47 \include{InductiveTypes.v}
adam@311 48 \include{Predicates.v}
adam@311 49 \include{Coinductive.v}
adam@353 50 \include{Subset.v}
adam@350 51 \include{GeneralRec.v}
adam@311 52 \include{MoreDep.v}
adam@311 53 \include{DataStruct.v}
adam@311 54 \include{Equality.v}
adam@311 55 \include{Generic.v}
adam@311 56 \include{Universes.v}
adam@324 57 \include{LogicProg.v}
adam@311 58 \include{Match.v}
adam@311 59 \include{Reflection.v}
adam@311 60 \include{Large.v}
adam@381 61 \include{ProgLang.v}
adam@383 62 \include{Conclusion.v}
adam@311 63
adam@311 64 \clearpage
adam@311 65 \addcontentsline{toc}{chapter}{Bibliography}
adam@311 66 \bibliographystyle{plain}
adam@311 67 \bibliography{cpdt}
adam@311 68
adam@311 69 \clearpage
adam@311 70 \addcontentsline{toc}{chapter}{Index}
adam@311 71 \printindex
adam@311 72
adam@311 73 \end{document}