Bug#275983: "coqc -v7" doesn't work; missing v7 library

[Martin Ellis <m.a.ellis@ncl.ac.uk>]

On Monday 11 Oct 2004 13:29, Lionel Elie Mamane wrote:
> Package: coq
> Version: 8.0pl1-3
> Severity: normal
>
> lionelm@harif:~/surreal/code$ coqc -v7 surreal.v
> Warning: Cannot open /usr/lib/coq/states7
> Warning: Cannot open /usr/lib/coq/theories7
> Warning: Cannot open /usr/lib/coq/contrib7
> User error: Can't find file initial.coq on loadpath
>
> You probably only "forgot" to ship these directories in the
> package.

The coq7-libs package provides these files:

apt-cache show coq7-libs
...
 This package provides existing theories from Coq 7 in Coq 8, and
 allows proofs that were developed in Coq 7 to be used in Coq 8.
 It is also required to translate theories in Coq 7 syntax into
 the new syntax introduced in Coq 8.  However, this package does
 not need to be installed to use Coq 7.

Regards
Martin