--- a/book/Makefile	Fri Aug 29 13:42:37 2008 -0400
+++ b/book/Makefile	Fri Aug 29 14:24:38 2008 -0400
@@ -1,17 +1,31 @@
-MODULES    := Tactics StackMachine
-VS         := $(MODULES:%=%.v)
-GLOBALS    := .coq_globals
+MODULES_NODOC := Tactics
+MODULES_DOC   := StackMachine
+MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
+VS            := $(MODULES:%=src/%.v)
+VS_DOC        := $(MODULES_DOC:%=%.v)
+GLOBALS       := .coq_globals
 
-.PHONY: coq clean
+.PHONY: coq clean doc
 
 coq: Makefile.coq
 	make -f Makefile.coq
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -impredicative-set -dump-glob $(GLOBALS)" \
+		COQC = "coqc -I src -impredicative-set \
+			-dump-glob $(GLOBALS)" \
 		-o Makefile.coq
 
 clean:: Makefile.coq
 	make -f Makefile.coq clean
-	rm -f Makefile.coq .depend
+	rm -f Makefile.coq .depend $(GLOBALS) \
+		latex/*.sty latex/cpdt.*
+
+doc: latex/cpdt.dvi
+
+latex/cpdt.tex: $(VS)
+	cd src ; coqdoc --latex $(VS_DOC) \
+		-o ../latex/cpdt.tex
+
+latex/cpdt.dvi: latex/cpdt.tex
+	cd latex ; latex cpdt