Many files added. Symbolic links missing. examples and contrib missing due

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

diff --git a/helm/EXPORT/exportcoq/provacoqReals.v b/helm/EXPORT/exportcoq/provacoqReals.v
new file mode 100644 (file)
index 0000000..445f9f9
--- /dev/null
+++ b/helm/EXPORT/exportcoq/provacoqReals.v
@@ -0,0 +1,23 @@
+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.