LIB_MODS    := Tactics Nonterm Esets Emaps

MODS        := Tactics ListUtil Maps Machine Pointer AndersenModel AndersenSound AndersenIter Andersen \
	$(LIB_MODS:%=lib/%)
COQ_SOURCES := $(MODS:%=%.v)

GLOBALS     := .coq_globals

include Makefile.coq

Makefile.coq: Makefile $(COQ_SOURCES)
	coq_makefile $(COQ_SOURCES) \
		COQC = "coqc -dump-glob $(GLOBALS)" \
		>Makefile.coq

.PHONY: doc publish

doc:
	-mkdir doc
	coqdoc -d doc -g --glob-from .coq_globals $(COQ_SOURCES)

Andersen.ml: Andersen.vo
	coqc AndersenExtract >Andersen.ml

publish:
	cp Makefile *.v *.ml ../html/coq/src/
	cp doc/*.html ../html/coq/