Moreover, some users of Coq have published various documents that may be useful both to beginners and advanced users of Coq:
the Coq'Art, the first book dedicated to the Coq proof assistant (Yves Bertot, Pierre Castéran, 2004, Chinese version in 2009); Software Foundations, a Coq-based textbook on logic, functional programming and foundations of programming languages (Benjamin Pierce et al, 2007, with regular updates); Certified Programming with Dependent Types, a textbook about practical engineering with Coq (Adam Chlipala, 2008); Video tutorials (Andrej Bauer, 2011); Preuves de programmes en coq (Video lectures in french) (Yves Bertot, 2013); a tutorial browsable interactively as a Coq file (Mike Nahas, 2014); Coq in a Hurry (Yves Bertot, 2006); an old Tutorial, which is a commented interactive session which introduces basics on terms, proofs, and tactics (Gérard Huet, Gilles Kahn and Christine Paulin-Mohring); a Tutorial on Recursive Types in Coq (Eduardo Giménez, Pierre Castéran, 2006) and the associated examples; a bunch of Frequently Asked Questions; Cocorico!, the Coq wiki; A Gentle Introduction to Type Classes and Rewriting in Coq (Pierre Castéran, Matthieu Sozeau, 2012) and the associated examples for Coq 8.3 and 8.4.