           SPELL=coq
         VERSION=8.3pl3
          SOURCE="${SPELL}-${VERSION}.tar.gz"
   SOURCE_URL[0]=http://${SPELL}.inria.fr/distrib/V${VERSION}/files/${SOURCE}
     SOURCE_HASH=sha512:c80d9dd13fdeba632e8db3e49fb210546ddfc665b7a7dedbdaad1a1e2533e2e526871d8995837c4806f322eb7c4b86a7ac0762167bcec54ac90a06b3eb246b50
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
