]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqInit.v
* the main function MUST return 0 to communicate everything was OK
[helm.git] / helm / EXPORT / exportcoq / provacoqInit.v
1 Require Export Xml.
2
3 Print XML Module Disk "examples" Datatypes.
4 Print XML Module Disk "examples" DatatypesSyntax.
5 Print XML Module Disk "examples" Logic.
6 Print XML Module Disk "examples" LogicSyntax.
7 Print XML Module Disk "examples" Specif.
8 Print XML Module Disk "examples" SpecifSyntax.
9 Print XML Module Disk "examples" Peano.
10 Print XML Module Disk "examples" Wf.
11 Print XML Module Disk "examples" Prelude.
12 Print XML Module Disk "examples" Logic_Type.
13 Print XML Module Disk "examples" Logic_TypeSyntax.