X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FEXPORT%2Fexportcoq%2FprovacoqArith.v;fp=helm%2FEXPORT%2Fexportcoq%2FprovacoqArith.v;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=1fdc4f943ed93e4d860c3f624499806d7da90bdd;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/EXPORT/exportcoq/provacoqArith.v b/helm/EXPORT/exportcoq/provacoqArith.v
deleted file mode 100644
index 1fdc4f943..000000000
--- 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.