Initial

diff --git a/helm/EXPORT/export_Marseille_CCS/Makefile b/helm/EXPORT/export_Marseille_CCS/Makefile
new file mode 100644 (file)
index 0000000..7c30db4
--- /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 (executable)
index 0000000..24fce6c
--- /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 (file)
index 0000000..e440667
--- /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 (file)
index 0000000..3421cc0
--- /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 (executable)
index 0000000..8e64b90
--- /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 (file)
index 0000000..04244aa
--- /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 (file)
index 0000000..ee2f95e
--- /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 (executable)
index 0000000..3a0db3d
--- /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 (file)
index 0000000..03f5942
--- /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 (file)
index 0000000..76fe930
--- /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 (executable)
index 0000000..e015204
--- /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 (file)
index 0000000..1905884
--- /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 (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

diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh b/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh
new file mode 100755 (executable)
index 0000000..acd865a
--- /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 (file)
index 0000000..1b17a93
--- /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.