The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Adam Chlipala 
<adam AT chlipala.net>
 writes:
> I think your function definition has a typo, where the last two
> recursive arguments to [next] are reversed.

No, I really did mean to put them in that order.

Changing the order of the arguments certainly gives you something that
type-checks, but it's a different program which no longer illustrates
the problem.

Thanks,

  - a