all: objects theories

objects:
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Words.v
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Alternate.v
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Opposite.v
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Paired.v
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Shuffle.v
	coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Gilbreath.v
	echo "Load Verbose prova_Rocq_SHUFFLE." | coqtop.byte -R SHUFFLE Rocq.SHUFFLE

theories:
	./exporttheories.sh

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