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.