The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 06/05/2013 08:49 AM, AUGER Cédric wrote:
> I do not use "inversion" nor "inversion_clear" as it gives way too big
> proof terms (and not easy to read). I hope someone will rewrite it
> someday to make a better version.
This development may interest you:

  http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/

> Once again, I know what I do when I do this and take care that.
My point was that not that _you_ do not know how elimination of equality 
works, but for that _most beginners_ do not know that. Hence, it is 
probably not a very useful trick to recommend :).

Robbert