[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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: