]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqcontribOmega.v
* the main function MUST return 0 to communicate everything was OK
[helm.git] / helm / EXPORT / exportcoq / provacoqcontribOmega.v
1 Require Export Xml.
2
3 Require Omega.
4 Require Zlogarithm.
5 Require OmegaSyntax.
6 Require Zpower.
7
8 Print XML Module Disk "examples" Omega.
9 Print XML Module Disk "examples" Zlogarithm.
10 Print XML Module Disk "examples" OmegaSyntax.
11 Print XML Module Disk "examples" Zpower.