]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqZArith.v
cicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :)
[helm.git] / helm / EXPORT / exportcoq / provacoqZArith.v
1 Require Export Xml.
2
3 Require Wf_Z.
4 Require ZArith.
5 Require ZArith_dec.
6 Require Zmisc.
7 Require Zsyntax.
8 Require auxiliary.
9 Require fast_integer.
10 Require zarith_aux.
11
12 Print XML Module Disk "examples" Wf_Z.
13 Print XML Module Disk "examples" ZArith.
14 Print XML Module Disk "examples" ZArith_dec.
15 Print XML Module Disk "examples" Zmisc.
16 Print XML Module Disk "examples" Zsyntax.
17 Print XML Module Disk "examples" auxiliary.
18 Print XML Module Disk "examples" fast_integer.
19 Print XML Module Disk "examples" zarith_aux.