The Coq mailing list

[Stephane Glondu <steph AT glondu.net>]

Mateusz Malinowski a écrit :
> I have a problem with Coqdoc, when I type coqdoc x.v then my bash will
> inform me: 'Fatal error: the x.v is not a bytecode executable file'.
> Apart from this if I type coqdoc --glob-from x.v I'll get 'Unknown
> option --glob-from'. I'm wondering if someone had similar problems.

This sounds like a stripped executable linked with -custom.

> I'm currently using Fedora 7 and The Coq Proof Assistant, version
> 8.1pl3 and I installed Coq from rpm.

Did you install the Fedora package? If so, you should probably fill in a 
bug report against the Fedora package.

BTW, there is a beta available for the next version of Coq at:

  http://coq.inria.fr/V8.2beta/

There are also RPMs.


Cheers,

--
Stéphane