]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoq.v
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the...
[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.