]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcoq/provacoqReals.v
Bug in the management of substitutions into auto corrected.
[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.