Mercurial > cpdt > repo
annotate latex/cpdt.tex @ 487:8bfb27cf0121
Add explicit warning that Coq 8.4 or later is required
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 07 Jan 2013 15:23:16 -0500 |
| parents | 40a9a36844d6 |
| children | da576746c3ba |
| 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@311 | 22 \thispagestyle{empty} |
| adam@311 | 23 \mbox{}\vfill |
| adam@311 | 24 \begin{center} |
| adam@311 | 25 |
| adam@370 | 26 Copyright Adam Chlipala 2008-2012. |
| adam@311 | 27 |
| adam@311 | 28 |
| adam@311 | 29 This work is licensed under a |
| adam@311 | 30 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
| adam@311 | 31 Unported License. |
| adam@311 | 32 The license text is available at: |
| adam@311 | 33 |
| adam@311 | 34 \end{center} |
| adam@311 | 35 |
| adam@311 | 36 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center} |
| adam@311 | 37 |
| adam@311 | 38 \phantomsection |
| adam@311 | 39 \tableofcontents |
| adam@311 | 40 |
| adam@311 | 41 \include{Intro.v} |
| adam@311 | 42 \include{StackMachine.v} |
| adam@311 | 43 \include{InductiveTypes.v} |
| adam@311 | 44 \include{Predicates.v} |
| adam@311 | 45 \include{Coinductive.v} |
| adam@353 | 46 \include{Subset.v} |
| adam@350 | 47 \include{GeneralRec.v} |
| adam@311 | 48 \include{MoreDep.v} |
| adam@311 | 49 \include{DataStruct.v} |
| adam@311 | 50 \include{Equality.v} |
| adam@311 | 51 \include{Generic.v} |
| adam@311 | 52 \include{Universes.v} |
| adam@324 | 53 \include{LogicProg.v} |
| adam@311 | 54 \include{Match.v} |
| adam@311 | 55 \include{Reflection.v} |
| adam@311 | 56 \include{Large.v} |
| adam@381 | 57 \include{ProgLang.v} |
| adam@383 | 58 \include{Conclusion.v} |
| adam@311 | 59 |
| adam@311 | 60 \clearpage |
| adam@311 | 61 \addcontentsline{toc}{chapter}{Bibliography} |
| adam@311 | 62 \bibliographystyle{plain} |
| adam@311 | 63 \bibliography{cpdt} |
| adam@311 | 64 |
| adam@311 | 65 \clearpage |
| adam@311 | 66 \addcontentsline{toc}{chapter}{Index} |
| adam@311 | 67 \printindex |
| adam@311 | 68 |
| adam@311 | 69 \end{document} |