
############################################################################
# You can define your own path to COQBIN by creating a file called
# "settings.sh" and placing the right definitions into it, e.g.
#     COQBIN=/var/tmp/charguer/v8.4/bin/
# Note the use of a leading slash.

COQBIN=

-include settings.sh

#######################################################
# BINARIES

COQC=$(COQBIN)coqc
COQDEP=$(COQBIN)coqdep

#######################################################
# FILES

LIB=\
	LibTactics.v \
	LibAxioms.v \
	LibEqual.v \
	LibLogic.v \
	LibEpsilon.v \
	LibFunc.v \
	LibChoice.v \
	LibOperation.v \
	LibBool.v \
	LibReflect.v \
	LibUnit.v \
	LibProd.v \
	LibSum.v \
	LibOption.v \
	LibStruct.v \
	LibRelation.v \
	LibOrder.v \
	LibWf.v \
	LibNat.v \
	LibInt.v \
	LibStruct.v \
	LibList.v \
	LibListSorted.v \
	LibListZ.v \
	LibBag.v \
	LibSet.v \
	LibMultiset.v \
	LibMap.v \
	LibArray.v \
	LibGraph.v \
	LibPer.v \
	LibString.v \
	LibFset.v \
	LibVar.v \
	LibEnv.v \
	LibLN.v \
	LibHeap.v \
	LibCore.v

MORE=\
	LibFix.v \
	LibStream.v 

DEMO=\
	LibTacticsDemos.v \
	LibFixDemos.v \
	LibOtherDemos.v 

#	LibCoreDemos.v \

TACTICS=\
	LibTactics.v \
	LibTacticsDemos.v 

ALL= $(LIB) $(MORE) $(DEMO)


#######################################################
# TARGETS

.SUFFIXES: .v .vo .vio
.PHONY: all lib tactics demo depend

all: $(ALL:.v=.vo) 
lib: $(LIB:.v=.vo) 
quick: $(ALL:.v=.vio) 
demo: $(DEMO:.v=.vo) 
tactics: $(TACTICS:.v=.vo)

depend: .depend

.v.vo : .depend
	$(COQC) -R . TLC $<

.v.vio : .depend
	$(COQC) -quick -R . TLC $<
	
	
#######################################################
#DEPENDENCIES

.depend : $(ALL)
	$(COQDEP) -R . TLC $(ALL) > .depend


ifeq ($(findstring $(MAKECMDGOALS),depend clean),)
include .depend
endif

#######################################################
#CLEAN

clean_quick:
	@rm -f *.vio || echo ok

clean:
	@rm -f *.vo *.vio || echo ok
	@rm -f .depend || echo ok





# -async-proofs-j
