The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Extraction Implicit is broken in the default Coq, when you use functors or 
sealed modules. I think it's fixed in the trunk. 

-Greg

> On Jun 26, 2014, at 4:07 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
> 
>> 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