]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqReals.v
Bug fixed in the guarded_by_descructors function: in some cases the context
[helm.git] / helm / EXPORT / exportcoq / provacoqReals.v
1 Require Export Xml.
2
3 Require R_Ifp.
4 Require Raxioms.
5 Require Rdefinitions.
6 Require Rbase.
7 Require Rbasic_fun.
8 Require Rderiv.
9 Require Reals.
10 Require Rfunctions.
11 Require Rlimit.
12 Require TypeSyntax.
13
14 Print XML Module Disk "examples" R_Ifp.
15 Print XML Module Disk "examples" Raxioms.
16 Print XML Module Disk "examples" Rdefinitions.
17 Print XML Module Disk "examples" Rbase.
18 Print XML Module Disk "examples" Rbasic_fun.
19 Print XML Module Disk "examples" Rderiv.
20 Print XML Module Disk "examples" Reals.
21 Print XML Module Disk "examples" Rfunctions.
22 Print XML Module Disk "examples" Rlimit.
23 Print XML Module Disk "examples" TypeSyntax.