Bug#275983: "coqc -v7" doesn't work; missing v7 library
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
Reply to: