The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

I am using "Eval compute in ..." to compute a term of type nat which is 
defined in a complicated way but should reduce to (S O).  When all the 
intermediate definitions are made transparent the computation goes through 
but when I make one definition opaque by ending it with Qed. instead of 
Defined.  the "Eval compute" hangs. 

Isn't it supposed to terminate anyway with whatever expression in a normal 
form it ends up with without unfolding the opaque definition?

Vladimir.