The Coq mailing list

["Alexander, Samuel" <alexander AT math.ohio-state.edu>]

>> Just removing "in ... return ..." seems to work.

> I am wondering why it doesn't work when "in ... return..." is used.

To make matters even more mysterious, the definition at the bottom of the 
following file suffers the same problem, and this time just messing around 
with "in ... return ..." no longer fixes it:

http://www.math.osu.edu/~alexander/variadic/variadic3.txt

-Sam Alexander