The Coq mailing list

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

On 02/11/2014 08:43 PM, Kristopher Micinski wrote:
> Out of curiosity, I may be missing the current one, but is there any
> resource that systematically attempts to collect the more advanced
> features of Coq?  As an example, while working through SF and CPDT
> will teach you a lot, when you hop into real developments you need to
> learn a laundry list of other things, such as libraries (Penn's
> metatheory library, SSReflect, etc...), lesser documented features
> (type classes and coercions), and new theory (e.g., working with the
> homotopy type theory branch).
>    

I think it would be misleading to say that the elements you mention are 
essential for "real developments."  I've only ever used one of them, and 
I actively recommend against using at least one of them, though I'll be 
tactful and not reveal which. :)

The one I've used is coercions, which I think is simple enough that the 
Coq reference manual makes for a good tutorial.

CPDT really is meant to cover all the material for "real developments" 
in Coq that is not easy to pick up from the Coq manual.  Particular 
application domains have their own knowledge bases, but I think of all 
that as distinct from Coq as a tool.