helm/EXPORT/export_Rocq_CHECKER/Makefile

   1 all: objects theories
   2
   3 objects:
   4         coqc -R CHECKER Rocq.CHECKER CHECKER/Functions.v CHECKER/Checker.v
   5         echo "Load Verbose prova_Rocq_CHECKER." | coqtop.byte -R CHECKER Rocq.CHECKER
   6
   7 theories:
   8         ./exporttheories.sh
   9
  10 clean:
  11         rm -f *.vo CHECKER/*.vo