all: objects theories

objects:
	coqc -R CHECKER Rocq.CHECKER CHECKER/Functions.v CHECKER/Checker.v
	echo "Load Verbose prova_Rocq_CHECKER." | coqtop.byte -R CHECKER Rocq.CHECKER

theories:
	./exporttheories.sh

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