The Flocq library provides vernacular files formalizing multi-radix
multi-precision fixed- and floating-point arithmetic for the Coq proof
assistant.

This package is free software; you can redistribute it and/or modify it
under the terms of GNU Lesser General Public License (see the COPYING
file). Authors are Sylvie Boldo <sylvie.boldo@inria.fr> and Guillaume
Melquiond <guillaume.melquiond@inria.fr>.