helm/EXPORT/export_Rocq_SHUFFLE/Makefile

   1 all: objects theories
   2
   3 objects:
   4         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Words.v
   5         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Alternate.v
   6         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Opposite.v
   7         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Paired.v
   8         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Shuffle.v
   9         coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Gilbreath.v
  10         echo "Load Verbose prova_Rocq_SHUFFLE." | coqtop.byte -R SHUFFLE Rocq.SHUFFLE
  11
  12 theories:
  13         ./exporttheories.sh
  14
  15 clean:
  16         rm -f *.vo SHUFFLE/*.vo