The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Jeffrey Terrell wrote:
> Thanks for your help. There's a very good primer on pattern matching 
> in sections 2 and 3 of "A New Elimination Rule for the Calculus of 
> Inductive Constructions" by Barras et al. It references what appears 
> to be a primary source on pattern matching, namely Coquand's 1992 
> paper on "Pattern Matching with Dependent Types". Does anyone know 
> where I can obtain a copy of this paper?

I treat the subject in a more tutorial style in CPDT:
    http://adam.chlipala.net/cpdt/
You should find all the important design patterns there, including the 
one that was suggested in response to your question here.