Extensions
The official extensions to the Rocq Prover.
Teams
Rocq Standard Library
The Rocq Corelib and Standard Library team.
Hugo Herbelin
Maintainer
herbelin
Andres Erbsen
Maintainer
andres-erbsen
Anton Trunov
Maintainer
anton-trunov
Maintainer
MSoegtropIMC
Olivier Laurent
Maintainer
olaure01
Pierre Rousselin
Maintainer
Villetaneuse
Numbers
The Numbers library and notations.
Jason Gross
Maintainer
JasonGross
Guillaume Melquiond
Maintainer
silene
Pierre Roux
Maintainer
proux01
Reals
The maintainers of the Reals library.
Hugo Herbelin
Maintainer
herbelin
Guillaume Melquiond
Maintainer
silene
Laurent Théry
Maintainer
thery
Vincent Semeria
Maintainer
VincentSe
Rocq Extraction
The Rocq Extraction plugin team.
Kazuhiko Sakaguchi
Maintainer
pi8027
Hugo Herbelin
Maintainer
herbelin
Automatic Tactic Plugins
The maintainers of the official plugins providing automatic tactics.
Pierre Corbineau
Maintainer (congruence, firstorder, rtauto)
PierreCorbineau
Assia Mahboubi
Maintainer (ring)
amahboubi
Maintainer (ring)
bgregoir
Frédéric Besson
Maintainer (micromega)
fajb
Hugo Herbelin
Maintainer (congruence, firstorder, nsatz, ring, rtauto)
herbelin
Pierre-Marie Pédrot
Maintainer (nsatz)
ppedrot
Laurent Théry
Maintainer (micromega, nsatz, ring)
thery