-
waterproof-dev Public
Forked from impermeable/waterproof-devDevelopment environment setup for coq-waterproof
Makefile GNU Lesser General Public License v3.0 UpdatedFeb 4, 2026 -
rocq Public
Forked from rocq-prover/rocqCoq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
-
coq-tactician Public
Forked from coq-tactician/coq-tacticianA Seamless, Interactive Tactic Learner and Prover for Coq
OCaml MIT License UpdatedFeb 4, 2026 -
rocq-lsp Public
Forked from rocq-community/rocq-lspLanguage Server Protocol for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedFeb 4, 2026 -
rocq-stdlib Public
Forked from rocq-prover/stdlibStdlib for the Rocq Prover
Rocq Prover GNU Lesser General Public License v2.1 UpdatedFeb 3, 2026 -
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
Rocq Prover GNU Lesser General Public License v2.1 UpdatedFeb 3, 2026 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA plugin for Coq to add dependent pattern-matching.
Rocq Prover GNU Lesser General Public License v2.1 UpdatedFeb 3, 2026 -
unicoq Public
Forked from unicoq/unicoqAn enhanced unification algorithm for Coq
OCaml MIT License UpdatedJan 30, 2026 -
coq-waterproof Public
Forked from impermeable/coq-waterproofCoq GNU Lesser General Public License v3.0 UpdatedJan 30, 2026 -
-
rewriter Public
Forked from mit-plv/rewriterReflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq Other UpdatedJan 30, 2026 -
-
ocaml-lsp Public
Forked from ocaml/ocaml-lspOCaml Language Server Protocol implementation
OCaml Other UpdatedDec 26, 2025 -
opam-coq-archive Public
Forked from rocq-prover/opamArchive for all Coq related OPAM packages organized in various repositories
-
paramcoq Public
Forked from rocq-community/paramcoqCoq plugin for parametricity
-
rocq-lean-import Public
Forked from rocq-community/rocq-lean-importOCaml GNU Lesser General Public License v2.1 UpdatedNov 25, 2025 -
coq-simple-io Public
Forked from Lysxia/coq-simple-ioIO for Gallina
Coq MIT License UpdatedNov 23, 2025 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
-
smtcoq Public
Forked from smtcoq/smtcoqCommunication between Coq and SAT/SMT solvers
OCaml Other UpdatedNov 20, 2025 -
vsrocq Public
Forked from rocq-prover/vsrocqA Visual Studio Code extension for Coq [maintainers=@maximedenes,@fakusb]
OCaml MIT License UpdatedNov 19, 2025 -
coqhammer Public
Forked from lukaszcz/coqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Automation for Dependent Type Theory
OCaml Other UpdatedNov 19, 2025 -
-
proofgeneral Public
Forked from ProofGeneral/PGThis repo is a fork of Proof General
Emacs Lisp GNU General Public License v3.0 UpdatedNov 10, 2025 -
ocaml-opam Public
Forked from ocaml/opam-repositoryMain public package repository for opam, the source package manager of OCaml.
Creative Commons Zero v1.0 Universal UpdatedNov 7, 2025 -
bot Public
Forked from rocq-prover/botA (Coq Development Team) bot written in OCaml
OCaml MIT License UpdatedNov 5, 2025 -
MetaRocq Public
Forked from MetaRocq/metarocqMetaprogramming in Coq
Coq MIT License UpdatedOct 30, 2025 -
category-theory Public
Forked from jwiegley/category-theoryAn axiom-free formalization of category theory in Coq for personal study and practical work
Coq BSD 3-Clause "New" or "Revised" License UpdatedOct 30, 2025 -
bedrock2 Public
Forked from mit-plv/bedrock2A work-in-progress language and compiler for verified low-level programming
Coq MIT License UpdatedOct 30, 2025 -
smpl Public
Forked from uds-psl/smplA Coq plugin providing an extensible tactic similar to first.
Coq MIT License UpdatedOct 29, 2025 -
coq-dpdgraph Public
Forked from rocq-community/coq-dpdgraphBuild dependency graphs between COQ objects
Coq GNU Lesser General Public License v2.1 UpdatedOct 29, 2025
{{ message }}