Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at PPS - Université Paris 7, January 2010.
Equations is a plugin for Coq implementing a dependent pattern-matching compiler and a set of tools generating support proofs for these definitions. I presented the prototype  and a paper describes the features and the implementation of the tool . A very preliminary tutorial is available too.
The code is available through a