The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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.