]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/EXPORT/exportcoq/provacoq.v
Many files added. Symbolic links missing. examples and contrib missing due
[helm.git] / helm / EXPORT / exportcoq / provacoq.v
diff --git a/helm/EXPORT/exportcoq/provacoq.v b/helm/EXPORT/exportcoq/provacoq.v
new file mode 100644 (file)
index 0000000..99b52eb
--- /dev/null
@@ -0,0 +1,14 @@
+Load Verbose provacoqArith.
+Load Verbose provacoqBool.
+Load Verbose provacoqInit.
+Load Verbose provacoqLists.
+Load Verbose provacoqLogic.
+Load Verbose provacoqReals.
+Load Verbose provacoqRelations.
+Load Verbose provacoqSets.
+(*Load Verbose provacoqSorting.*)
+(*Load Verbose provacoqTrees.*)
+Load Verbose provacoqZArith.
+
+Load Verbose provacoqcontribRing.
+Load Verbose provacoqcontribOmega.