A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.