The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

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?

> I have a project which uses extraction, and works around the inability
> of "Extraction Implicit" to deal with certain issues - collectively
> referred to as erasability.  If you are interested:
> https://github.com/jonleivent/mindless-coding.
> 
> -- Jonathan
> 
>