The Coq mailing list

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

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?

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?

Best Regards
CSS