Skip to content

@rocq-prover The Rocq Prover

Change the repository type filter

All

    Repositories list

    22 repositories

    • vsrocq

      Public
      Visual Studio Code extension for Coq
      editorcoqvscodevscode-extensionvscodiumrocqrocq-prover
      OCaml
      •
      MIT License
      •81•388•147•13•Updated Jun 5, 2025Jun 5, 2025

    • doc

      Public
      Coq user manual, automatically deployed
      HTML
      •1•0•0•0•Updated Jun 4, 2025Jun 4, 2025

    • bot

      Public
      The Rocq Prover bot
      githubbotgithub-apigitlabwebhookocamlgitlab-apigithub-app
      OCaml
      •
      MIT License
      •16•23•113•5•Updated Jun 4, 2025Jun 4, 2025

    • 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 theorems together with an environment for semi-interactive development of machine-checked proofs.
      dependent-typescoqtheorem-provingproof-assistant
      OCaml
      •
      GNU Lesser General Public License v2.1
      •683•5.1k•2.6k•84•Updated Jun 4, 2025Jun 4, 2025

    • stdlib

      Public
      Stdlib for the Rocq Prover
      Coq
      •
      GNU Lesser General Public License v2.1
      •14•14•77•14•Updated Jun 4, 2025Jun 4, 2025

    • opam

      Public
      Archive for all Rocq and Coq-related opam packages organized in various repositories
      coqopam-repositoryopamrocq-prover
      OCaml
      •
      GNU Lesser General Public License v2.1
      •135•142•34•6•Updated Jun 4, 2025Jun 4, 2025

    • rocq-prover.org

      Public
      The Rocq Prover Website
      HTML
      •
      Other
      •20•11•20•5•Updated Jun 3, 2025Jun 3, 2025

    • platform-docs

      Public
      A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
      Coq
      •
      Other
      •16•21•43•7•Updated May 28, 2025May 28, 2025

    • platform

      Public
      Multi platform setup for Coq, Coq libraries and tools
      Shell
      •
      Creative Commons Zero v1.0 Universal
      •51•203•46•14•Updated May 28, 2025May 28, 2025

    • 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
      •38•17•1•0•Updated Jan 20, 2025Jan 20, 2025

    • rfcs

      Public
      Rocq RFCs: documents to discuss changes to the Rocq Prover
      rfcrocq-prover
      35•57•3•50•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
      10•31•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