X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexport_Rocq_SHUFFLE%2FMakefile;fp=helm%2FEXPORT%2Fexport_Rocq_SHUFFLE%2FMakefile;h=ba2ab57121610245230157fa984aaaae8b50b090;hb=88748cdbea1609de367a1e034606207d66b70508;hp=0000000000000000000000000000000000000000;hpb=40e7943e21872051f6a88cba2a1e9faa6492b6a3;p=helm.git

diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/Makefile b/helm/EXPORT/export_Rocq_SHUFFLE/Makefile
new file mode 100644
index 000000000..ba2ab5712
--- /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