all: objects theories

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

theories:
	./exporttheories.sh

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