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).
Guillaume Melquiond
authored
Name | Last commit | Last update |
---|---|---|
src | ||
testsuite | ||
.gitignore | ||
AUTHORS | ||
COPYING | ||
INSTALL | ||
NEWS | ||
README | ||
Remakefile.in | ||
autogen.sh | ||
configure.in | ||
remake.cpp |