--- /dev/null
+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