The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

You can do Show Proof just before Qed to get the exact term that has to be typechecked at Qed (I think).

Trying to type-check parts of the proof-term might help in isolating the problem.

-- Abhishek

On Mon, Oct 28, 2013 at 6:41 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi,

In theory, a one tactic script can generate an arbitrarily complex proof term (which is checked at Qed), so you should give more information (like the lemma and its proof) if you want some advice.

Maxime.

On 10/28/2013 06:35 PM, Marcus Ramos wrote:

Hi,

It takes a few minutes to run the demonstration of a lemma with a few lines in it, but when it reaches "Qed", it takes more than 40 minutes just for it. Why is that so?

Thanks in advance,
Marcus.