[2] On October 11, 2023, the development team announced that Coq will be renamed The Rocq Prover in coming months, and began updating the code base, website, and associated tools.

The development of Coq was initiated by Gérard Huet and Thierry Coquand, and more than 40 people, mainly researchers, have contributed features to the core system since its inception.

The implementation team has successively been coordinated by Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin, and Matthieu Sozeau.

[11] Their work led to the development of the SSReflect ("Small Scale Reflection") package, which was a significant extension to Coq.

These features include: SSReflect 1.11 is freely available, dual-licensed under the open source CeCILL-B or CeCILL-2.0 license, and compatible with Coq 8.11.

[13] In addition to constructing Gallina terms explicitly, Coq supports the use of tactics written in the built-in language Ltac or in OCaml.