FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli  \
	evm_compute.mli evm_compute.ml  \
	 coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \
	aac.mlpack \
	AAC.v  Instances.v Tutorial.v Caveats.v 

ARGS := -R . AAC_tactics

.PHONY: coq clean doc

world: all doc

all: Makefile.coq
	$(MAKE) -f Makefile.coq all

install: Makefile.coq
	$(MAKE) -f Makefile.coq install

coq: Makefile.coq
	$(MAKE) -f Makefile.coq

doc: Makefile.coq
	$(MAKE) -f Makefile.coq html
	$(MAKE) -f Makefile.coq mlihtml

Makefile.coq: Makefile $(VS)
	coq_makefile $(ARGS) $(FILES) -o Makefile.coq

clean:: Makefile.coq
	$(MAKE) -f Makefile.coq clean
	rm -f Makefile.coq .depend