Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.

This package contains shared files and the commandline interface. For GTK graphical interface install %{name}-ide.