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