The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Thomas Schilling wrote:
> I'm working through Adam's Certified Programming with Dependent Types and Coq 
> fails to accept the following definition from the book:
> [...]
>
> Is this a limitation of my version of Coq?  I'm using Coq 8.2pl1 (latest on 
> MacPorts).  Or am I missing something obvious?
>    

The book is only tested with Coq 8.2pl2 and 8.3pl1.  There were 
definitely some bugs in 8.2pl1 that prevented some of the code from 
type-checking, though I don't remember seeing your particular example 
mentioned before.