UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Mathematical Components - Library of formalized mathematics for the Coq system.

QuickChick - Randomized Property-Based Testing Plugin for Coq.

CoqHammer - Automated Reasoning Hammer Tool for Coq.

coq-ext-lib - Library of Coq definitions, theorems, and tactics.

Tricks in Coq - Some tips, tricks, and features in Coq that are hard to discover.

MetaCoq - Metaprogramming in Coq.

Fiat - Deductive Synthesis of Abstract Data Types in a Proof Assistant.

Equations - Function definition package for Coq.

Proofs - Selection of formal developments in Coq.