Metaprogramming, verified meta-theory and implementation of Coq in Coq

proof script associated to tutorial material

A Coq library providing tactics to deal with hypothesis

Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

A collection of tools for writing technical documents that mix Coq code and prose.

Pocklington's criterion for primality in Coq [maintainer=@Casteran]

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.