X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;fp=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=445f9f9883f6801952d7cba3441107497b902559;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git

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.