The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
This not usual. I would guess that your problem is something like
you ask
Eval compute in (fun (x : foo) => bar x)
and that's immediate but in the hypothesis of your proof you don't have 
x : foo 
but
x := term_that_allow_very_heavy_computation : foo
so
compute "bar x" -> compute "bar term_that_allow_very_heavy_computation" takes 
ages

It is impossible to make more useful comments without a concrete example of 
your problem.

All the best,
Pierre B.

Le 26 sept. 2013 à 02:37, Marcus Ramos 
<mvmramos AT gmail.com>
 a écrit :

> 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.