This commit was manufactured by cvs2svn to create branch 'moogle'.

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

diff --git a/helm/EXPORT/exportcoq/provacoqRelations.v b/helm/EXPORT/exportcoq/provacoqRelations.v
deleted file mode 100644 (file)
index c588b30..0000000
--- 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.*)