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=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=c588b30f3d7f107703f4243547b32e07b4d170a3;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git

diff --git a/helm/EXPORT/exportcoq/provacoqRelations.v b/helm/EXPORT/exportcoq/provacoqRelations.v
deleted file mode 100644
index c588b30f3..000000000
--- a/helm/EXPORT/exportcoq/provacoqRelations.v
+++ /dev/null
@@ -1,33 +0,0 @@
-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.*)