]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoq.v
crosso compatibility patch which enable building both with ocaml 3.08 and 3.09
[helm.git] / helm / EXPORT / exportcoq / provacoq.v
1 Load Verbose provacoqArith.
2 Load Verbose provacoqBool.
3 Load Verbose provacoqInit.
4 Load Verbose provacoqLists.
5 Load Verbose provacoqLogic.
6 Load Verbose provacoqReals.
7 Load Verbose provacoqRelations.
8 Load Verbose provacoqSets.
9 (*Load Verbose provacoqSorting.*)
10 (*Load Verbose provacoqTrees.*)
11 Load Verbose provacoqZArith.
12
13 Load Verbose provacoqcontribRing.
14 Load Verbose provacoqcontribOmega.