X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;fp=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;h=0000000000000000000000000000000000000000;hp=445f9f9883f6801952d7cba3441107497b902559;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/EXPORT/exportcoq/provacoqReals.v b/helm/EXPORT/exportcoq/provacoqReals.v
deleted file mode 100644
index 445f9f988..000000000
--- a/helm/EXPORT/exportcoq/provacoqReals.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Export Xml.
-
-Require R_Ifp.
-Require Raxioms.
-Require Rdefinitions.
-Require Rbase.
-Require Rbasic_fun.
-Require Rderiv.
-Require Reals.
-Require Rfunctions.
-Require Rlimit.
-Require TypeSyntax.
-
-Print XML Module Disk "examples" R_Ifp.
-Print XML Module Disk "examples" Raxioms.
-Print XML Module Disk "examples" Rdefinitions.
-Print XML Module Disk "examples" Rbase.
-Print XML Module Disk "examples" Rbasic_fun.
-Print XML Module Disk "examples" Rderiv.
-Print XML Module Disk "examples" Reals.
-Print XML Module Disk "examples" Rfunctions.
-Print XML Module Disk "examples" Rlimit.
-Print XML Module Disk "examples" TypeSyntax.