Commit 438bf9d4 authored by Adam Chlipala's avatar Adam Chlipala

Proper title and copyright pages

parent ff307eca
......@@ -23,9 +23,12 @@ clean:: Makefile.coq
doc: latex/cpdt.dvi latex/cpdt.pdf html
latex/cpdt.tex: $(VS)
latex/cpdt.tex: Makefile $(VS)
cd src ; coqdoc --latex $(VS_DOC) \
-p "\usepackage{url}" -toc \
-p "\usepackage{url}" \
-p "\title{Certified Programming with Dependent Types}" \
-p "\author{Adam Chlipala}" \
-p "\iffalse" \
-o ../latex/cpdt.tex
latex/cpdt.dvi: latex/cpdt.tex
......@@ -34,7 +37,7 @@ latex/cpdt.dvi: latex/cpdt.tex
latex/cpdt.pdf: latex/cpdt.dvi
cd latex ; pdflatex cpdt
html: $(VS)
html: Makefile $(VS)
cd src ; coqdoc $(VS_DOC) -toc \
--glob-from ../$(GLOBALS) \
-d ../html
......
......@@ -7,8 +7,20 @@
* http://creativecommons.org/licenses/by-nc-nd/3.0/
*)
(** %\fi
\begin{document}
\maketitle
\thispagestyle{empty}
\mbox{}\vfill
\begin{center}% *)
(**
Copyright Adam Chlipala 2008.
This work is licensed under a
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
Unported License.
......@@ -18,6 +30,15 @@ The license text is available at:
*)
(** %\vfill\mbox{}
\end{center}
\tableofcontents
\chapter{Introduction}% *)
(** * Whence This Book? *)
......@@ -148,7 +169,7 @@ This book is generated automatically from Coq source files using the wonderful c
There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition:
%\begin{center}\url{http://adam.chlipala.net/cpdt/html/}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/">http://adam.chlipala.net/cpdt/html/</a></tt></blockquote>#
The chapters of this book are named like "Module Foo," rather than having proper names, because literally the entire document is generated by coqdoc, which by default bases chapter structure on the module structure of the development being documented. This chapter is headed "Module Intro" because it comes from a module named [Intro], which comes from a fascinating source file %\texttt{%#<tt>#Intro.v#</tt>#%}% containing nothing but specially-formatted coqdoc comments.
The chapters of this book are named like "Module Foo," rather than having proper names, because literally the entire document is generated by coqdoc, which by default bases chapter structure on the module structure of the development being documented. The next chapter is headed "Module StackMachine" because it comes from a module named [StackMachine], which comes from a source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}%.
The source code to the book is also freely available at:
%\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote>#
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment