helm/EXPORT/exportprove/Makefile

   1 all: objects theories
   2
   3 objects:
   4         coqc -R prove prove prove/*.v
   5         echo "Load Verbose provaStruct." | ~/V7/bin/coqtop.byte -R prove prove
   6         echo "Load Verbose provaFeIota." | ~/V7/bin/coqtop.byte -R prove prove
   7         echo "Load Verbose provaCofix." | ~/V7/bin/coqtop.byte -R prove prove
   8         echo "Load Verbose prova." | ~/V7/bin/coqtop.byte -R prove prove
   9
  10 theories:
  11         ./exporttheories.sh
  12
  13 clean:
  14         rm -f *.vo prove/*.vo