Pretty LaTeX generation

.hgignore

@@ -6,3 +6,8 @@ syntax: glob
 *.vo
 */Makefile.coq
 */.coq_globals
+
+*/coqdoc.sty
+*/cpdt.*
+*/*.log
+

book/Makefile

-MODULES    := Tactics StackMachine
-VS         := $(MODULES:%=%.v)
+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

book/StackMachine.v → book/src/StackMachine.v

@@ -7,14 +7,18 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
+(* begin hide *)
 Require Import List.
 
 Require Import Tactics.
+(* end hide *)
 
 
 (** * Arithmetic expressions over natural numbers *)
 
+(* begin hide *)
 Module Nat.
+(* end hide *)
   (** ** Source language *)
 
   Inductive binop : Set := Plus | Times.
@@ -112,4 +116,6 @@ Module Nat.
     reflexivity.
   Qed.
 
+(* begin hide *)
 End Nat.
+(* end hide *)