# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220474271 14400
# Node ID 00366a62bd005bc096c428ba78e59af67020f4f1
# Parent  c0cbf324ec7d25990a56ac44dd4bf662274f20f9
Proper title and copyright pages

diff -r c0cbf324ec7d -r 00366a62bd00 Makefile
--- a/Makefile	Wed Sep 03 16:14:47 2008 -0400
+++ b/Makefile	Wed Sep 03 16:37:51 2008 -0400
@@ -23,9 +23,12 @@
 
 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.pdf: latex/cpdt.dvi
 	cd latex ; pdflatex cpdt
 
-html: $(VS)
+html: Makefile $(VS)
 	cd src ; coqdoc $(VS_DOC) -toc \
 		--glob-from ../$(GLOBALS) \
 		-d ../html
diff -r c0cbf324ec7d -r 00366a62bd00 src/Intro.v
--- a/src/Intro.v	Wed Sep 03 16:14:47 2008 -0400
+++ b/src/Intro.v	Wed Sep 03 16:37:51 2008 -0400
@@ -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 @@
 
 *)
 
+(** %\vfill\mbox{}
+\end{center}
+
+\tableofcontents
+
+\chapter{Introduction}% *)
+
+
+
 
 (** * Whence This Book? *)
 
@@ -148,7 +169,7 @@
 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>#