package coq-gappa

You can search for identifiers within the package.

in-package search v0.2.0

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

Install

Dune Dependency

gappa.gitlabpages.inria.fr Edit opam file Versions (24)

Authors

G

Guillaume Melquiond <guillaume.melquiond@inria.fr>

Maintainers

G

guillaume.melquiond@inria.fr

Sources

gappalib-coq-1.11.0.tar.gz

sha512=654d4787998ce085b8ce7e6f6c266e826e9581b34002c1c0995972a3927800e5732f8e6205ea63047aca84327413f4e2f774e2c5627fe7b98fba809250c0b857

Description

Tags

keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2026-06-02

Published: 02 Jun 2026

Dependencies (7)

conf-clang build
conf-g++ build
coq-flocq >= "4.1"
coq-core
coq >= "8.16" & < "8.17~"
ocamlfind build
ocaml

Dev Dependencies (1)

conf-autoconf build & dev

Used by

None

Conflicts

None

On This Page

Description
Dependencies (7)
Dev Dependencies (1)
Used by
Conflicts