The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi,
I have some question about coercions with tactics. I have tried to 
exploit coercions within some tactics but unfortunately it does not work.
All tactics I have tried (rewrite, replace, ...) are based on equality 
of terms while others (e.g., change) perform conversions based on universes.
So, if someone has an idea about a possibility to cope with coercions in 
tactics?
Thanks in advance,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard