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 -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
