The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hello,

Is it possible to define a conversion tactic [1] that could be used with 
Eval? It can be useful to combine unfold, simpl...

For instance:

Ltac foo := unfold bar; simpl.
Eval foo in foobar.

Thanks,
Chantal.

[1] http://coq.inria.fr/refman/Reference-Manual011.html#Conversion-tactics