The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

This is a bug, thanks for the report. This error message should not stop 
the compilation of your files however, does it?

Are your libraries accessible, so that we can reproduce the bug? (you 
can send me a link privately)

Maxime.

On 01/23/2014 08:50 AM, 
drg AT illinois.edu
 wrote:
> Using the latest version of coq on the trunk, and building a library after
> building and installing another, I get this error message:
>
> $ coqc  -q  -R . Ktheory   Utilities
> File "./NKtheory_Utilities.native", line 39, characters 34-110:
> Error: Unbound module NFoundations_Generalities_uu0
> Error: Could not compile the library to native code. Skipping.
>
> I suspect the makefile made by coq_makefile isn't making the files *.native
> properly available.  If so, where should I put them?