The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

The following works:

Goal True.
let N := 3 in do N idtac 0.
Abort.

It produces 3 lines of "0".

So, why doesn't the following work?:

Goal True.
let N := eval compute in (1 + 2) in do N idtac 0.
Abort.

It produces the error: "Error: Ltac variable N is bound to a term which 
cannot be coerced to an integer.", with CoqIDE underlining the N in "do 
N idtac 0" as the source of the error.

How does one compute with integers in Ltac?

-- Jonathan