]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqSorting.v
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the...
[helm.git] / helm / EXPORT / exportcoq / provacoqSorting.v
1 (*
2 Require Export Xml.
3
4 Require Generic.
5 Require Heap.
6 Require Permutation.
7 Require Sorting.
8
9 Print XML Module Disk "examples" Generic.
10 Print XML Module Disk "examples" Heap.
11 Print XML Module Disk "examples" Permutation.
12 Print XML Module Disk "examples" Sorting.
13 *)