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

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

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