gappalib-coq

This package contains a Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.