From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Dec 2000 15:23:08 +0000 (+0000)
Subject: Initial
X-Git-Tag: nogzip~81
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88748cdbea1609de367a1e034606207d66b70508;p=helm.git

Initial
---

diff --git a/helm/EXPORT/export_Marseille_CCS/Makefile b/helm/EXPORT/export_Marseille_CCS/Makefile
new file mode 100644
index 000000000..7c30db4a5
--- /dev/null
+++ b/helm/EXPORT/export_Marseille_CCS/Makefile
@@ -0,0 +1,11 @@
+all: objects theories
+
+objects:
+	coqc -R CCS Marseille.CCS CCS/*.v
+	echo "Load Verbose prova_Marseille_CCS." | coqtop.byte -R CCS Marseille.CCS
+
+theories:
+	./exporttheories.sh
+
+clean:
+	rm -f *.vo CCS/*.vo
diff --git a/helm/EXPORT/export_Marseille_CCS/exporttheories.sh b/helm/EXPORT/export_Marseille_CCS/exporttheories.sh
new file mode 100755
index 000000000..24fce6c39
--- /dev/null
+++ b/helm/EXPORT/export_Marseille_CCS/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in CCS/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Marseille/CCS/$basename" > \
+   examples/Marseille/CCS/$basename.theory.xml
+ done
diff --git a/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v b/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v
new file mode 100644
index 000000000..e44066736
--- /dev/null
+++ b/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v
@@ -0,0 +1,5 @@
+Require Export Xml.
+
+Require Trans_Sys.
+
+Print XML Module Disk "examples" Trans_Sys.
diff --git a/helm/EXPORT/export_Nijmegen_Rem/Makefile b/helm/EXPORT/export_Nijmegen_Rem/Makefile
new file mode 100644
index 000000000..3421cc0a6
--- /dev/null
+++ b/helm/EXPORT/export_Nijmegen_Rem/Makefile
@@ -0,0 +1,11 @@
+all: objects theories
+
+objects:
+	coqc -R Rem Nijmegen.Rem Rem/*.v
+	echo "Load Verbose prova_Nijmegen_Rem." | coqtop.byte -R Rem Nijmegen.Rem
+
+theories:
+	./exporttheories.sh
+
+clean:
+	rm -f *.vo Rem/*.vo
diff --git a/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh
new file mode 100755
index 000000000..8e64b90c5
--- /dev/null
+++ b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in Rem/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Nijmegen/Rem/$basename" > \
+   examples/Nijmegen/Rem/$basename.theory.xml
+ done
diff --git a/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v b/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v
new file mode 100644
index 000000000..04244aa30
--- /dev/null
+++ b/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v
@@ -0,0 +1,5 @@
+Require Export Xml.
+
+Require Rem.
+
+Print XML Module Disk "examples" Rem.
diff --git a/helm/EXPORT/export_Paris_ZF/Makefile b/helm/EXPORT/export_Paris_ZF/Makefile
new file mode 100644
index 000000000..ee2f95e1b
--- /dev/null
+++ b/helm/EXPORT/export_Paris_ZF/Makefile
@@ -0,0 +1,25 @@
+all: objects theories
+
+objects:
+	coqc -R ZF/src Paris.ZF ZF/src/nothing.v
+	coqc -R ZF/src Paris.ZF ZF/src/useful.v
+	coqc -R ZF/src Paris.ZF ZF/src/ZFbasis.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_extensionnalite.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_paire.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_reunion.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_parties.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_comprehension.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_remplacement.v
+	coqc -R ZF/src Paris.ZF ZF/src/couples.v
+	coqc -R ZF/src Paris.ZF ZF/src/applications.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_choice.v
+	coqc -R ZF/src Paris.ZF ZF/src/axs_fundation.v
+	coqc -R ZF/src Paris.ZF ZF/src/ZFrelations.v
+	coqc -R ZF/src Paris.ZF ZF/src/MSetBasis.v
+	echo "Load Verbose prova_Paris_ZF." | coqtop.byte -R ZF/src Paris.ZF
+
+theories:
+	./exporttheories.sh
+
+clean:
+	rm -f *.vo ZF/src/*.vo
diff --git a/helm/EXPORT/export_Paris_ZF/exporttheories.sh b/helm/EXPORT/export_Paris_ZF/exporttheories.sh
new file mode 100755
index 000000000..3a0db3d49
--- /dev/null
+++ b/helm/EXPORT/export_Paris_ZF/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in ZF/src/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Paris/ZF/$basename" > \
+   examples/Paris/ZF/$basename.theory.xml
+ done
diff --git a/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v b/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v
new file mode 100644
index 000000000..03f59427f
--- /dev/null
+++ b/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v
@@ -0,0 +1,33 @@
+Require Export Xml.
+
+Require nothing.
+Require useful.
+Require ZFbasis.
+Require axs_extensionnalite.
+Require axs_paire .
+Require axs_reunion.
+Require axs_parties.
+Require axs_comprehension.
+Require axs_remplacement.
+Require couples.
+Require applications .
+Require axs_choice.
+Require axs_fundation.
+Require ZFrelations.
+Require MSetBasis .
+
+Print XML Module Disk "examples" nothing.
+Print XML Module Disk "examples" useful.
+Print XML Module Disk "examples" ZFbasis.
+Print XML Module Disk "examples" axs_extensionnalite.
+Print XML Module Disk "examples" axs_paire .
+Print XML Module Disk "examples" axs_reunion.
+Print XML Module Disk "examples" axs_parties.
+Print XML Module Disk "examples" axs_comprehension.
+Print XML Module Disk "examples" axs_remplacement.
+Print XML Module Disk "examples" couples.
+Print XML Module Disk "examples" applications .
+Print XML Module Disk "examples" axs_choice.
+Print XML Module Disk "examples" axs_fundation.
+Print XML Module Disk "examples" ZFrelations.
+Print XML Module Disk "examples" MSetBasis .
diff --git a/helm/EXPORT/export_Rocq_CHECKER/Makefile b/helm/EXPORT/export_Rocq_CHECKER/Makefile
new file mode 100644
index 000000000..76fe9308a
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_CHECKER/Makefile
@@ -0,0 +1,11 @@
+all: objects theories
+
+objects:
+	coqc -R CHECKER Rocq.CHECKER CHECKER/Functions.v CHECKER/Checker.v
+	echo "Load Verbose prova_Rocq_CHECKER." | coqtop.byte -R CHECKER Rocq.CHECKER
+
+theories:
+	./exporttheories.sh
+
+clean:
+	rm -f *.vo CHECKER/*.vo
diff --git a/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh b/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh
new file mode 100755
index 000000000..e0152041f
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in CHECKER/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Rocq/CHECKER/$basename" > \
+   examples/Rocq/CHECKER/$basename.theory.xml
+ done
diff --git a/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v b/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v
new file mode 100644
index 000000000..190588474
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v
@@ -0,0 +1,7 @@
+Require Export Xml.
+
+Require Functions.
+Require Checker.
+
+Print XML Module Disk "examples" Functions.
+Print XML Module Disk "examples" Checker.
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
diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh b/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh
new file mode 100755
index 000000000..acd865a42
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in SHUFFLE/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Rocq/SHUFFLE/$basename" > \
+   examples/Rocq/SHUFFLE/$basename.theory.xml
+ done
diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v
new file mode 100644
index 000000000..1b17a93bc
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v
@@ -0,0 +1,16 @@
+Require Export Xml.
+
+Require Alternate.
+Require Gilbreath.
+Require Opposite.
+Require Paired.
+Require Shuffle.
+Require Words.
+
+
+Print XML Module Disk "examples" Alternate.
+Print XML Module Disk "examples" Gilbreath.
+Print XML Module Disk "examples" Opposite.
+Print XML Module Disk "examples" Paired.
+Print XML Module Disk "examples" Shuffle.
+Print XML Module Disk "examples" Words.