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

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

diff --git a/helm/EXPORT/exportcoq/provacoqArith.v b/helm/EXPORT/exportcoq/provacoqArith.v
deleted file mode 100644 (file)
index 1fdc4f9..0000000
--- a/helm/EXPORT/exportcoq/provacoqArith.v
+++ /dev/null
@@ -1,31 +0,0 @@
-Require Export Xml.
-
-Require Arith.
-Require Compare.
-Require Compare_dec.
-(*Require Div.*)
-Require Div2.
-Require EqNat.
-Require Euclid_def.
-Require Euclid_proof.
-Require Peano_dec.
-
-Print XML Module Disk "examples" Arith.
-Print XML Module Disk "examples" Between.
-Print XML Module Disk "examples" Compare.
-Print XML Module Disk "examples" Compare_dec.
-(*Print XML Module Disk "examples" Div.*)
-Print XML Module Disk "examples" Div2.
-Print XML Module Disk "examples" EqNat.
-Print XML Module Disk "examples" Euclid_def.
-Print XML Module Disk "examples" Euclid_proof.
-Print XML Module Disk "examples" Even.
-Print XML Module Disk "examples" Gt.
-Print XML Module Disk "examples" Le.
-Print XML Module Disk "examples" Lt.
-Print XML Module Disk "examples" Min.
-Print XML Module Disk "examples" Minus.
-Print XML Module Disk "examples" Mult.
-Print XML Module Disk "examples" Peano_dec.
-Print XML Module Disk "examples" Plus.
-Print XML Module Disk "examples" Wf_nat.