Bug#275983: "coqc -v7" doesn't work; missing v7 library
On Mon, Oct 11, 2004 at 01:46:29PM +0100, Martin Ellis wrote:
> On Monday 11 Oct 2004 13:29, Lionel Elie Mamane wrote:
>> 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
> >
> The coq7-libs package provides these files:
That's strange; I did a "dpkg -l '*coq*'" to look for such a package,
but it is not in the list:
lionelm@harif:~/surreal/code$ dpkg -l '*coq*'
ii coq 8.0pl1-3 Proof assistant for higher-order logic (toplevel and compiler)
ii coq-doc 8.0pl1.0-1 Documentation for Coq
ii coq-libs 8.0pl1-3 Proof assistant for higher-order logic (theories)
un coqide <none> (no description available)
ii proofgeneral-coq 3.5-3 ProofGeneral support for coq
I'm reassigning this to dpkg.
--
Lionel
Reply to: