The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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