The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have some python scripts at https://github.com/JasonGross/coq-bug-finder which automatically minimize an error-producing Coq file.  If you use them, let me know if you have any trouble.

-Jason

On Fri, Jun 27, 2014 at 12:01 AM, Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de> 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?

> 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
>
>