The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Chris,

I expect experts will have more to say about this, but in this
circumstance I always try  "make clean; make" or whatever other
incantation achieves a complete rebuild.

--Randy


On Tue, Aug 23, 2016 at 11:19 AM, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 wrote:
> Dear Chris,
>
>
>
> as far as I remember, there are 8.4 patch versions of Coq which are happy
> with  ‘ –Q “.” Top ‘ and others which insert an extra Top in the module name
> if you give this option (leave it away or give –Q “.” “” instead)
>
>
>
> A few notes on this which might help:
>
>
>
> -        The relation between Coq module paths and file system paths is
> controlled using the –Q and –R options. How this exactly works (especially
> how this influences the module path written into a .vo file) is not very
> well documented.
>
>
>
> -        some Coq 8.4 versions contain bugs in the –Q option, See bug
> reports
>
>
>
> https://coq.inria.fr/bugs/show_bug.cgi?id=3995
>
> https://coq.inria.fr/bugs/show_bug.cgi?id=3958
>
>
>
> Fixing this bug obviously changed the behavior of –Q and some things which
> did work before because the bug was there might stop working in Coq versions
> where the bug is fixed (and the other way around).
>
>
>
> -        As far as I can guess from my experience the Coq module name stored
> in a Coq vo file always contains a “Top” as root which is stripped away. So
> when Coq says your module is named “Top.X” it might be that it is actually
> “Top.Top.X”
>
>
>
> Best regards,
>
>
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928