]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/export_Rocq_SHUFFLE/Makefile
...
[helm.git] / 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