The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/26/2014 07:01 PM, Christoph-Simon Senjak wrote:
> Thank you for the immediate answer.
>
> > Are you suggesting that this failure occurs even when you don't have any
> > "Extraction Implicit" declarations?
> Yes, I do not use Extraction Implicit. Is that wrong?
>
> If so, I have to say that I use a git-version. Might this be a bug in
> that version?

It sounds like there is an "Extraction Implicit" declaration in 
something you are using.  If you can identify the modules you are 
requiring, can you search in their sources for "Extraction Implicit"?

I personally have not seen the "Extraction Implicit" error message occur 
without myself using an "Extraction Implicit" declaration, so that is my 
guess of what is happening with your project.  But, it could always be a 
bug - if there are no "Extraction Implicit" declarations in any modules 
you are using, and you still get that error message, I would encourage 
you to send that into the Coq bug list.

-- Jonathan