           SPELL=coq
         VERSION=8.4
          SOURCE="${SPELL}-${VERSION}.tar.gz"
   SOURCE_URL[0]=http://${SPELL}.inria.fr/distrib/V${VERSION}/files/${SOURCE}
     SOURCE_HASH=sha512:c9429ecb8c692d45c91d9c3dad093cb2e51f0af63ec99643eea584373156d0cd46a6e1eb278482e57dbf37ef59752506faa8485584445763e05d2ab06dfeab49
SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
        WEB_SITE="http://coq.inria.fr"
      LICENSE[0]=GPL
         ENTERED=20120302
           SHORT="a formal proof management system"
cat << EOF
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the formalization of programming languages semantics (e.g.
the CompCert compiler certification project or Java Card EAL7 certification
in industrial context), the formalization of mathematics (e.g. the full
formalization of the 4 color theorem or constructive mathematics at Nijmegen)
and teaching.
EOF
