Two main documents are officially maintained by the Coq development team:

• the Reference Manual, which is the complete, authoritative source of documentation for Coq;
• the documentation of the Standard Library distributed with the system.

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 (and only) book dedicated to the Coq proof assistant (Yves Bertot, Pierre Castéran, May 2004);
• Certified Programming with Dependent Types, a textbook about practical engineering with Coq (Adam Chlipala, 2008);
• Coq in a Hurry (Yves Bertot, May 2006);
• a 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, Aug 2006) and the associated examples;
• a bunch of Frequently Asked Questions;
• Cocorico!, the Coq wiki.