X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;fp=helm%2FEXPORT%2Fexportcoq%2FprovacoqReals.v;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=445f9f9883f6801952d7cba3441107497b902559;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;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.