The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Cedric,

> Is there someone working on having such proof term generation?
> I admit, that before doing my inversion I put my goal in a special form
> (in fact I went the furthest as possible without requiring to use
> inversion, so that using inversion will be done on the smallest type)
> 
> I may be wrong, but I believe that there is no tactic doing this now.
> If I am wrong, please tell it me, so my proofs will be a lot lighter
> (I never use the manual trick I did here).
> 
> If you think such a tactic would be cool, I would be glad to try to
> implement it (I never programmed directly a tactic in OCaml).

I believe Pierre Boutillier is working on improving inversion to do 
exactly that.

-- Matthieu