Initial

[helm.git] / helm / EXPORT / export_Rocq_SHUFFLE / Makefile

diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/Makefile b/helm/EXPORT/export_Rocq_SHUFFLE/Makefile
new file mode 100644 (file)
index 0000000..ba2ab57
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_SHUFFLE/Makefile
@@ -0,0 +1,16 @@
+all: objects theories
+
+objects:
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Words.v
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Alternate.v
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Opposite.v
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Paired.v
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Shuffle.v
+       coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Gilbreath.v
+       echo "Load Verbose prova_Rocq_SHUFFLE." | coqtop.byte -R SHUFFLE Rocq.SHUFFLE
+
+theories:
+       ./exporttheories.sh
+
+clean:
+       rm -f *.vo SHUFFLE/*.vo