Mentions légales du service

Skip to content
Snippets Groups Projects
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).