[benwr]

This tutorial starts by explaining how things work, and only later shows you magic. That's exactly what I like about it, actually. Almost every coq tutorial I found (I tried software foundations, cpdt, and several shorter online tutorials) fails to explain what you're doing before you do it.

[tom_mellior]

Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.