The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/26/2014 06:23 PM, Christoph-Simon Senjak wrote:
> Hello.
>
> I am trying to extract a term from my (very long) code, and I get the
> error message
>
>      Error: The 2nd argument of exist still occurs after extraction.
>      Please check the Extraction Implicit declarations.
>
> (How) can I find out what part of my program causes the problem?

I don't think there is any way to find out why an Extraction Implicit 
declaration fails.  And it certainly can fail in non-obvious ways.

> As my coding style is very similar everywhere, there will probably many
> instances of the same problem (the same error already occured on other
> functions I tested). Is it - instead - possible to just extract
> everything, including Prop-Terms, so it does not have to bother about these?

Are you suggesting that this failure occurs even when you don't have any 
"Extraction Implicit" declarations?  If not, just remove the "Extraction 
Implicit" declarations and retry the extraction.

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