This support library provides vernacular files so that the certificates Gappa
generates can be imported by the Coq proof assistant. It also provides a
"gappa" tactic that calls Gappa on the current Coq goal.

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques --
automatic proof generation of arithmetic properties) is a tool intended to
help verifying and formally proving properties on numerical programs dealing
with floating-point or fixed-point arithmetic.

The online documentation is available at:

	http://gappa.gforge.inria.fr/doc/

Gappa support library for the Coq proof assistant is free software; you can
redistribute it and/or modify it under the terms of GNU Lesser General Public
License (see the COPYING file).
