]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqBool.v
if a node has an xref use it for cut and paste, no matter if it have an href as well
[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.