]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqBool.v
new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...
[helm.git] / helm / EXPORT / exportcoq / provacoqBool.v
1 Require Export Xml.
2
3 Require Bool.
4 Require DecBool.
5 Require IfProp.
6 Require Sumbool.
7 Require Zerob.
8
9 Print XML Module Disk "examples" Bool.
10 Print XML Module Disk "examples" DecBool.
11 Print XML Module Disk "examples" IfProp.
12 Print XML Module Disk "examples" Sumbool.
13 Print XML Module Disk "examples" Zerob.