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.*)