The Coq mailing list

["Marcus Ramos" <mvmramos AT gmail.com>]

Hi,

When I issue an "Eval compute" on a term with a call to a single Fixpoint, the
answer is almost immediate.

When I issue "compute" (for the same Fixpoint with the same arguments) inside
a proof for a theorem, it takes a long while (>15 minutes) and finally I get
the message "Invalid argument" (stack overflow?). Because of this, I can´t
complete the proof of the theorem.

Is this usual? Any hints why this happens? How could I trace the problem and
fix it? I am using coqIDE 8.4pl1 in Windows 8.

Thanks in advance,
Marcus.