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

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


These files are now provided by the coq7-libs package (most users don't need them). Maybe could we do a hack to explain that when the -v7 flag is used and the files are not present.



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.

Reply to: