ACKS

VCFloat depends on the following external libraries,
which are normally supplied by the Coq Platform installation
(either by opam or by other means):

- The CompCert C verified compiler.

  Copyright (C) 2004-2022 INRIA.

  VCFloat can be built and used with or without CompCert.
  Some components of VCFloat (and some applications of VCFloat) need 
  CompCert, other components (and applications) do not.

  Those parts of VCFloat that depend on CompCert, require only
  CompCert's dual-licensed components:  that is, the portion of CompCert
  that is licensed by either/both the (open-source) GNU Lesser Public License
  and the (not open-source) INRIA License.  See the CompCert
  distribution for explanations of licenses.

- Flocq, a Floating-Point Library for Coq.

  Copyright (C) 2010-2022 Sylvie Boldo and Guillaume Melquiond.

  Flocq is distributed under the GNU Lesser General Public License,
  (GNU LGPL) version 3.0 (reproduced verbatim in extenso below).

- Coq-Interval, an Interval Package for Coq.

  Copyright (C) 2007-2022 Guillaume Melquiond.

  Coq-Interval is distributed under the CeCILL-C free software
  license (reproduced verbatim in cecill-c.txt).