The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

This repo is the new home of Proof General

Multi platform setup for Coq, Coq libraries and tools

Docker images of coq-mathcomp [maintainer=@erikmd]

The HOL Light theorem prover

Archive for all Rocq and Coq-related opam packages organized in various repositories