The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.jussieu.fr>]

Hi all,

> On 2011/04/07, at 22:39, Benjamin C. Pierce wrote:
> > ... but are there situations where inversion doesn't work and  
> > destruct does?


I see one indirect limitation :
inversion used to be not friend with the "fix" tactic because
inversion rewrites equality over arguments of the inductive and
> fix f x := match x with
> |C y => f (eq_rect bli bla blo y)
> end
wasn't accepted by <= v8.3 guard condition. (In trunk, guard condition  
handles commutative cuts)


Pierre Boutillier
pierre.boutillier AT pps.jussieu.fr