Rocq Runtime
The Rocq Runtime team is responsible for the development and maintenance of the Rocq kernel and elaboration (rocq-runtime and rocq-equations).
Teams
Rocq Kernel and Trusted Code Base
The kernel-maintainers, library-maintainers (vo file loading), universes-maintainers, and vm-native-maintainers teams.
Gaëtan Gilbert
Maintainer (kernel, library, universes)
SkySkimmer
Erik Martin-Dorel
Maintainer (vm-native)
erikmd
Matthieu Sozeau
Maintainer (universes)
mattam82
Pierre-Marie Pédrot
Maintainer (kernel, universes, vm-native)
ppedrot
Pierre Roux
Maintainer (vm-native)
proux01
Guillaume Melquiond
Maintainer (library, vm-native)
silene
Yann Leray
Maintainer (kernel)
yannl35133
Rocq Elaboration
The derive-maintainers, engine-maintainers, extensible-syntax-maintainers, funind-maintainers, ltac-maintainers, parsing-maintainers, pretyper-maintainers, tactics-maintainers, typeclasses-maintainers, and vernac-maintainers teams.
Pierre Courtieu
Maintainer (funind)
Matafou
Gaëtan Gilbert
Maintainer (engine, ltac, vernac)
SkySkimmer
Arnaud Spiwack
Maintainer (derive)
aspiwack
Maintainer (funind)
forestjulien
Enrico Tassi
Maintainer (pretyper)
gares
Hugo Herbelin
Maintainer (derive, engine, extensible-syntax, ltac, parsing, tactics)
herbelin
Matthieu Sozeau
Maintainer (extensible-syntax, pretyper, tactics, typeclasses, vernac)
mattam82
Pierre-Marie Pédrot
Maintainer (derive, engine, ltac, parsing, pretyper, tactics, typeclasses)
ppedrot
Pierre Roux
Maintainer (extensible-syntax)
proux01
Ltac2
The Ltac2 tactic language team.
Pierre-Marie Pédrot
Team leader
ppedrot
Kenji Maillard
Maintainer
kyoDralliam
Jason Gross
Maintainer
JasonGross
Tej Chajed
Maintainer
tchajed
Gaëtan Gilbert
Maintainer
SkySkimmer
Maintainer
MSoegtropIMC
SSReflect
The SSReflect proof language team.
Cyril Cohen
Maintainer
CohenCyril
Enrico Tassi
Maintainer
gares
Georges Gonthier
Maintainer
ggonthier