coq-gappa

• 1.2.1
• 1.3.2
• 1.3.3
• 1.3.4
• 1.4.0
• 1.4.1
• 1.4.2
• 1.4.2+8.11
• 1.4.3
• 1.4.4
• 1.4.5
• 1.4.6

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

opam install coq-gappa.1.4.6

homepage

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

license

LGPL-3.0-or-later

bugs tracker

https://gitlab.inria.fr/gappa/coq/issues

dependencies

"ocaml" "ocamlfind" {build} "coq" {>= "8.8.1" & < "8.14~"} "coq-flocq" {>= "3.0"} "conf-autoconf" {build & dev} ("conf-g++" {build} | "conf-clang" {build})

source

https://gforge.inria.fr/frs/download.php/file/38386/gappalib-coq-1.4.6.tar.gz

package

https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-gappa/coq-gappa.1.4.6