Skip to content

@rocq-prover The Rocq Prover

Change the repository type filter

All

    Repositories list

    25 repositories

    • doc

      Public
      Rocq documentation, automatically deployed
      HTML
      •1•1•0•0•Updated Jul 6, 2026Jul 6, 2026

    • rocq

      Public
      The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and…
      dependent-typescoqtheorem-proving
      dependent-typescoqtheorem-provingproof-assistant
      OCaml
      •
      GNU Lesser General Public License v2.1
      •742•5.5k•2.5k•92•Updated Jul 6, 2026Jul 6, 2026

    • vsrocq

      Public
      Visual Studio Code extension for Coq
      editorcoqvscode
      editorcoqvscodevscode-extensionvscodiumrocqrocq-prover
      OCaml
      •
      MIT License
      •106•455•171•23•Updated Jul 6, 2026Jul 6, 2026

    • stdlib

      Public
      Stdlib for the Rocq Prover
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •37•38•83•15•Updated Jul 6, 2026Jul 6, 2026

    • equations

      Public
      A function definition package for Rocq
      programming-languagedependent-typescoq
      programming-languagedependent-typescoqrocq
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •58•238•86•8•Updated Jul 2, 2026Jul 2, 2026

    • opam

      Public
      Archive for all Rocq and Coq-related opam packages organized in various repositories
      coqopam-repositoryopam
      coqopam-repositoryopamrocq-prover
      OCaml
      •
      GNU Lesser General Public License v2.1
      •135•172•31•10•Updated Jul 2, 2026Jul 2, 2026

    • rocq-prover.org

      Public
      The Rocq Prover Website
      HTML
      •
      Other
      •28•15•25•4•Updated Jul 2, 2026Jul 2, 2026

    • platform

      Public
      Multi platform setup for Rocq, Rocq libraries and tools
      Shell
      •
      Creative Commons Zero v1.0 Universal
      •55•238•55•13•Updated Jun 23, 2026Jun 23, 2026

    • bot

      Public
      The Rocq Prover bot
      githubbotgithub-api
      githubbotgithub-apigitlabwebhookocamlgitlab-apigithub-app
      OCaml
      •
      MIT License
      •15•29•114•5•Updated Jun 13, 2026Jun 13, 2026

    • platform-docs

      Public
      A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
      Rocq Prover
      •
      Other
      •22•26•44•7•Updated Jun 2, 2026Jun 2, 2026

    • rocq-platform-starter

      Public
      One-command bootstrap installer for reproducible Rocq Platform environments across Linux, macOS and Windows.
      Go
      •
      MIT License
      •0•5•0•0•Updated May 13, 2026May 13, 2026

    • docker-opam-action

      Public
      GitHub Action using Docker-Coq [maintainers=@Justme0606,@Zimmi48]
      continuous-integrationcoqopam
      continuous-integrationcoqopamactiongithub-actionsdocker-coqcontainer-cidocker-coq-action
      Shell
      •
      MIT License
      •5•15•23•3•Updated Apr 30, 2026Apr 30, 2026

    • deploy-rocq-prover.org

      Public
      OCurrent deployment pipeline for rocq-prover.org
      OCaml
      •
      MIT License
      •0•0•0•0•Updated Mar 27, 2025Mar 27, 2025

    • coq.github.io

      Public
      Source files of the previous coq.inria.fr website
      HTML
      •
      Other
      •37•18•1•0•Updated Jan 20, 2025Jan 20, 2025

    • rfcs

      Public
      Rocq RFCs: documents to discuss changes to the Rocq Prover
      rfcrocq-prover
      rfcrocq-prover
      37•64•3•53•Updated Jan 15, 2025Jan 15, 2025

    • coq-on-cachix

      Public
      This repository follows Coq active branches but is only updated when the latest commit is available as binary on https://coq.cachix.org
      OCaml
      •
      GNU Lesser General Public License v2.1
      •1•3•0•0•Updated Jul 1, 2022Jul 1, 2022

    • prerequisites

      Public
      This repository is only used to store tarballs of dependencies of the Coq Platform (see https://github.com/coq/platform).
      0•0•0•0•Updated Sep 17, 2021Sep 17, 2021

    • coq-bench

      Public archive
      Scripts for differential performance testing of Coq packages / versions
      Shell
      •
      Other
      •6•4•0•0•Updated Sep 8, 2021Sep 8, 2021

    • ltac2

      Public
      A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository.
      coq-plugin
      coq-plugin
      9•33•0•0•Updated Jun 5, 2019Jun 5, 2019

    • repo-coqs-disabled

      Public archive
      The repository for Coq versions for developers.
      Dockerfile
      •
      MIT License
      •2•1•1•0•Updated Sep 3, 2018Sep 3, 2018

    • roadmaps

      Public archive
      This was used to prepare the versions 8.6-8.8.
      1•2•0•0•Updated Feb 26, 2018Feb 26, 2018

    • opam-coq-shell

      Public archive
      attempt to create a simplified shell for opam when installing coq
      Shell
      •
      GNU Lesser General Public License v2.1
      •2•0•2•0•Updated Jul 5, 2015Jul 5, 2015

    • repo-unstable-disabled

      Public archive
      The repository for development packages.
      MIT License
      •6•3•0•0•Updated Jun 27, 2015Jun 27, 2015

    • repo-stable-disabled

      Public archive
      The repository for stable Coq packages.
      MIT License
      •7•9•0•0•Updated Jun 27, 2015Jun 27, 2015

    • repo-8.5

      Public archive
      2•0•0•1•Updated Apr 15, 2015Apr 15, 2015
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.