adamc@3: MODULES_NODOC := Tactics
adamc@4: MODULES_DOC   := Intro StackMachine
adamc@3: MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
adamc@3: VS            := $(MODULES:%=src/%.v)
adamc@3: VS_DOC        := $(MODULES_DOC:%=%.v)
adamc@3: GLOBALS       := .coq_globals
adamc@2: 
adamc@4: .PHONY: coq clean doc dvi html
adamc@2: 
adamc@2: coq: Makefile.coq
adamc@2: 	make -f Makefile.coq
adamc@2: 
adamc@2: Makefile.coq: Makefile $(VS)
adamc@2: 	coq_makefile $(VS) \
adamc@3: 		COQC = "coqc -I src -impredicative-set \
adamc@3: 			-dump-glob $(GLOBALS)" \
adamc@2: 		-o Makefile.coq
adamc@2: 
adamc@2: clean:: Makefile.coq
adamc@2: 	make -f Makefile.coq clean
adamc@3: 	rm -f Makefile.coq .depend $(GLOBALS) \
adamc@3: 		latex/*.sty latex/cpdt.*
adamc@3: 
adamc@4: doc: latex/cpdt.dvi html
adamc@3: 
adamc@3: latex/cpdt.tex: $(VS)
adamc@3: 	cd src ; coqdoc --latex $(VS_DOC) \
adamc@4: 		-p "\usepackage{url}" \
adamc@3: 		-o ../latex/cpdt.tex
adamc@3: 
adamc@3: latex/cpdt.dvi: latex/cpdt.tex
adamc@3: 	cd latex ; latex cpdt
adamc@4: 
adamc@4: html: $(VS)
adamc@4: 	cd src ; coqdoc $(VS_DOC) \
adamc@4: 		--glob-from ../$(GLOBALS) \
adamc@4: 		-d ../html
adamc@4: 
adamc@4: dvi:
adamc@4: 	xdvi latex/cpdt