A Coq Library on Floating-Point Arithmetic

This library was first designed by Laurent Théry and Laurence Rideau. Contributors now include Laurent Fousse, Guillaume Melquiond and Sylvie Boldo (maintainer).

The following graph, made using dot, describes the dependences between all the files of the library. All the nodes are clickable to access directly the file.
The colors refer to the directory where the file lie and to the subject matter: beige for the initial library, green for the expansions, violet for the two's complement, blue for the elementary functions evaluation and red for the other files.