The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Randy,

This is bug #4335 [1] where you can follow the discussion. This is
related to native compilation so a quick workaround is to configure
coq with native compilation disabled.

Best,

Hugo

[1] https://coq.inria.fr/bugs/show_bug.cgi?id=4335

On Mon, Jan 23, 2017 at 05:56:57PM +0000, Randy Pollack wrote:
> Consider the following two files.  Coq 8.5pl1 with ProofGeneral fails
> to load file_XXX.v
> 
> The definitions are just to make the example non-trivial, but the
> [Require] seem to be relevant.
> 
> BTW, I tried to log in to Bugzilla, but failed.
> 
> --Randy
> 
> =====file_XXX.v=======================
> Module XXX.
> 
> Require Bool.
> 
> Load file_YYY.
> Export YYY.
> 
> Definition tt := true.
> 
> End XXX.
> =====================================
> 
> ------file_YYY.v---------------------
> Module YYY.
> 
> Definition ff := false.
> 
> End YYY.
> --------------------------