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

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

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