The Coq mailing list

[Assia Mahboubi <assia.mahboubi AT inria.fr>]

Hi,

I would like to inspect the values produced on particular entries by a 
tactic constructing terms, like:

Ltac toto n := constr:(S n).

I can  build an other  tactic :

Ltac titi n :=
let x := (toto n) in
let m := fresh "m" in (pose m := x).

and call it in proof mode.

I would like to know if there is a simpler way to access to the values 
of toto.

Thanks in advance,


assia