]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/EXPORT/exportcoq/provacoqBool.v
Many files added. Symbolic links missing. examples and contrib missing due
[helm.git] / helm / EXPORT / exportcoq / provacoqBool.v
diff --git a/helm/EXPORT/exportcoq/provacoqBool.v b/helm/EXPORT/exportcoq/provacoqBool.v
new file mode 100644 (file)
index 0000000..a898237
--- /dev/null
@@ -0,0 +1,13 @@
+Require Export Xml.
+
+Require Bool.
+Require DecBool.
+Require IfProp.
+Require Sumbool.
+Require Zerob.
+
+Print XML Module Disk "examples" Bool.
+Print XML Module Disk "examples" DecBool.
+Print XML Module Disk "examples" IfProp.
+Print XML Module Disk "examples" Sumbool.
+Print XML Module Disk "examples" Zerob.