all: objects theories

objects:
	coqc -R prove prove prove/*.v
	echo "Load Verbose provaStruct." | ~/V7/bin/coqtop.byte -R prove prove
	echo "Load Verbose provaFeIota." | ~/V7/bin/coqtop.byte -R prove prove
	echo "Load Verbose provaCofix." | ~/V7/bin/coqtop.byte -R prove prove
	echo "Load Verbose prova." | ~/V7/bin/coqtop.byte -R prove prove

theories:
	./exporttheories.sh

clean:
	rm -f *.vo prove/*.vo