Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportcoq / provacoqSets.v

diff --git a/helm/EXPORT/exportcoq/provacoqSets.v b/helm/EXPORT/exportcoq/provacoqSets.v
new file mode 100644 (file)
index 0000000..9502861
--- /dev/null
+++ b/helm/EXPORT/exportcoq/provacoqSets.v
@@ -0,0 +1,48 @@
+Require Export Xml.
+
+Require Classical_sets.
+Require Constructive_sets.
+Require Cpo.
+Require Ensembles.
+Require Finite_sets.
+Require Finite_sets_facts.
+Require Image.
+Require Infinite_sets.
+Require Integers.
+Require Multiset.
+Require Partial_Order.
+Require Permut.
+(*Require CSCPermut.*)
+Require Powerset.
+Require Powerset_Classical_facts.
+Require Powerset_facts.
+Require Relations_1.
+Require Relations_1_facts.
+Require Relations_2.
+Require Relations_2_facts.
+Require Relations_3.
+Require Relations_3_facts.
+Require Uniset.
+
+Print XML Module Disk "examples" Classical_sets.
+Print XML Module Disk "examples" Constructive_sets.
+Print XML Module Disk "examples" Cpo.
+Print XML Module Disk "examples" Ensembles.
+Print XML Module Disk "examples" Finite_sets.
+Print XML Module Disk "examples" Finite_sets_facts.
+Print XML Module Disk "examples" Image.
+Print XML Module Disk "examples" Infinite_sets.
+Print XML Module Disk "examples" Integers.
+Print XML Module Disk "examples" Multiset.
+Print XML Module Disk "examples" Partial_Order.
+Print XML Module Disk "examples" Permut.
+Print XML Module Disk "examples" Powerset.
+Print XML Module Disk "examples" Powerset_Classical_facts.
+Print XML Module Disk "examples" Powerset_facts.
+Print XML Module Disk "examples" Relations_1.
+Print XML Module Disk "examples" Relations_1_facts.
+Print XML Module Disk "examples" Relations_2.
+Print XML Module Disk "examples" Relations_2_facts.
+Print XML Module Disk "examples" Relations_3.
+Print XML Module Disk "examples" Relations_3_facts.
+Print XML Module Disk "examples" Uniset.