X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexportcoq%2FprovacoqRelations.v;fp=helm%2FEXPORT%2Fexportcoq%2FprovacoqRelations.v;h=c588b30f3d7f107703f4243547b32e07b4d170a3;hb=5cc1f56f25e23f8132b578f9ad46ac9e27979cb4;hp=0000000000000000000000000000000000000000;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git

diff --git a/helm/EXPORT/exportcoq/provacoqRelations.v b/helm/EXPORT/exportcoq/provacoqRelations.v
new file mode 100644
index 000000000..c588b30f3
--- /dev/null
+++ b/helm/EXPORT/exportcoq/provacoqRelations.v
@@ -0,0 +1,33 @@
+Require Export Xml.
+
+Require Newman.
+Require Operators_Properties.
+Require Relation_Definitions.
+Require Relation_Operators.
+Require Relations.
+Require Rstar.
+(*Require Disjoint_Union.*)
+(*Require Inclusion.*)
+(*Require Inverse_Image.*)
+(*Require Lexicographic_Exponentiation.*)
+(*Require Lexicographic_Product.*)
+(*Require Transitive_Closure.*)
+(*Require Union.*)
+(*Require Well_Ordering.*)
+(*Require Wellfounded.*)
+
+Print XML Module Disk "examples" Newman.
+Print XML Module Disk "examples" Operators_Properties.
+Print XML Module Disk "examples" Relation_Definitions.
+Print XML Module Disk "examples" Relation_Operators.
+Print XML Module Disk "examples" Relations.
+Print XML Module Disk "examples" Rstar.
+(*Print XML Module Disk "examples/WELLFOUNDED" Disjoint_Union.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Inclusion.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Inverse_Image.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Exponentiation.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Product.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Transitive_Closure.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Union.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Well_Ordering.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Wellfounded.*)