Exact real arithmetic in Coq

Here is the Coq developpement of the library : exactreals.tgz
Download the archive.
Extract the files.
Compile using make.

It should be used with the development version of Coq (I use the revision 10428).
There are two examples of proof using the library in the file testbasis.v.
Algorithms are described in realbasis.v.

I will add (more) informations as soon as possible.