Bug#538398: coq: The description in README.Debian about proofgeneral is old.
Package: coq
Version: 8.2.pl1+dfsg-2
Severity: minor
* A description of the incorrect behavior:
/usr/share/doc/coq/README.Debian says that there is no official Debian
package of Proof General yet.
>Coq frontends
>-------------
>For interactive use of coqtop, we suggest
>- either the Debian cle package
>- or the Proof-General (x)emacs mode, which unfortunately can not be
>distributed by Debian for copyright reasons. However, a Debian package
>might become available at proof general home page in the future
>(http://zermelo.dcs.ed.ac.uk/~proofgen)
But this information is old. The package proofgeneral-coq is available
now and coq recommends this package. Please update this section of
README.Debian.
* A suggested fix:
I found a diff in the net. See
https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/trunk/distrib/debian/README.Debian?root=coq&rev=3637&r1=2288&r2=3637
-- System Information:
Debian Release: squeeze/sid
APT prefers unstable
APT policy: (500, 'unstable')
Architecture: i386 (i686)
Versions of packages coq depends on:
ii coq-theories 8.2.pl1+dfsg-2 proof assistant for higher-order l
ii emacsen-common 1.4.19 Common facilities for all emacsen
ii libc6 2.9-21 GNU C Library: Shared libraries
ii ocaml-base-nox [ocaml-bas 3.11.1-2 Runtime system for OCaml bytecode
Versions of packages coq recommends:
ii coqide 8.2.pl1+dfsg-2 proof assistant for higher-order l
ii proofgeneral-coq 3.7-3 generic interface for proof assist
Versions of packages coq suggests:
ii coq-doc 8.1-3 documentation for Coq in html form
pn libcoq-ocaml-dev <none> (no description available)
ii ocaml-nox 3.11.1-2 ML implementation with a class-bas
ii proofgeneral-coq 3.7-3 generic interface for proof assist
ii rlwrap [readline-editor] 0.30-1.1 readline feature command line wrap
Reply to: