R := ..

.PHONY: coq check all doc clean lscoqfiles

M := CertC CoqAddOn Itv PositiveMapAddOn LinTerm Ring_polynom_AddOn \
	NumC ProgVar OptionMonad Debugging Impure ImpureConfig \
	DomainInterfaces CstrC ConsSet Backend \
	ASTerm ASAtomicCond ASCond AssignD \
	PedraQ PedraZ DemoPLVerifier ZNone ZNoneItv PredTrans \
	DomainGCL LinearizeBackend


V := $(addsuffix .v, $(M))
VO := $(addsuffix .vo, $(M))
GLOB := $(addsuffix .glob, $(M))
DV := $(addsuffix .dv, $(M))

coq: $(VO)

DemoExtract.vo: $(VO) DemoExtract.v
	cd Exec; coqc -I ../ ../DemoExtract.v

DemoPLTests.vo: DemoPLVerifier.vo DemoPLTests.v

DemoExtractTests.vo: $(VO) DemoExtract.vo DemoPLTests.vo DemoExtractTests.v
	cd Exec; coqc -I ../ ../DemoExtractTests.v

check: DemoExtractTests.vo
	$(MAKE) -C Exec all

# additional developments...
all: check DemoPLPredTransTheory.vo TestPolynom.vo

doc: $(VO)
	if test ! -d doc; then mkdir doc; fi
	coqdoc -d doc $(V)

%.vo: %.v
	coqc $<

%.dv: %.v
	coqdep -I . $< > $@

lscoqfiles:
	@echo ${M}

clean:
	$(MAKE) -C Exec allclean
	rm -rf doc
	rm -f *.vo *.dv *.glob *~

include $(DV)
