]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqLogic.v
* the main function MUST return 0 to communicate everything was OK
[helm.git] / helm / EXPORT / exportcoq / provacoqLogic.v
1 Require Export Xml.
2
3 Require Classical.
4 Require Classical_Pred_Set.
5 Require Classical_Pred_Type.
6 Require Classical_Prop.
7 Require Classical_Type.
8 Require Eqdep.
9 Require Eqdep_dec.
10
11 Print XML Module Disk "examples" Classical.
12 Print XML Module Disk "examples" Classical_Pred_Set.
13 Print XML Module Disk "examples" Classical_Pred_Type.
14 Print XML Module Disk "examples" Classical_Prop.
15 Print XML Module Disk "examples" Classical_Type.
16 Print XML Module Disk "examples" Eqdep.
17 Print XML Module Disk "examples" Eqdep_dec.