This directory contains a number of .v files illustrating small inversion techniques presented on http://www-verimag.imag.fr/~monin/Talks/sir.pdf with some extensions.

Basically:

* an improvement on CoqWS 2010 and ITP 2013, using auxiliary inductives rather than their CPS translation which suits many practical needs; 
* a less easy but still compact approach which is usable in combination with the guard condition of recursive programs, designed for the Braga method (joint work with Dominique Larchey-Wendling).
    
    
Both versions are able to deal with cases which seem out of reach of Coq standard inversion.