-
coq 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…
OCaml GNU Lesser General Public License v2.1 UpdatedDec 9, 2025 -
dune Public
Forked from ocaml/duneA composable build system for OCaml.
OCaml MIT License UpdatedDec 6, 2025 -
-
ocaml-imagelib Public
The imagelib library implements image formats such as PNG or PPM
-
ocaml-earley-ocaml Public
Extensible OCaml parser to be used with Earley
-
ocaml-earley Public
Parsing library based on Earley Algorithm
-
-
-
-
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
OCaml GNU Lesser General Public License v2.1 UpdatedSep 24, 2024 -
hierarchy-builder Public
Forked from math-comp/hierarchy-builderHigh level commands to declare a hierarchy based on packed classes
Prolog MIT License UpdatedSep 11, 2024 -
elpi Public
Forked from LPCIC/elpiEmbeddable Lambda Prolog Interpreter
Prolog GNU Lesser General Public License v2.1 UpdatedSep 11, 2024 -
coq-ext-lib Public
Forked from rocq-community/coq-ext-libA library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Coq BSD 2-Clause "Simplified" License UpdatedSep 4, 2024 -
ocaml-bindlib Public
Efficient binder representation in OCaml
-
vscoq Public
Forked from rocq-prover/vsrocqA Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]
OCaml MIT License UpdatedJun 18, 2024 -
coq-lsp Public
Forked from ejgallego/rocq-lspVisual Studio Code Extension and Language Server Protocol for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedJun 13, 2024 -
coq-tactician Public
Forked from coq-tactician/coq-tacticianA Seamless, Interactive Tactic Learner and Prover for Coq
OCaml MIT License UpdatedJun 13, 2024 -
metacoq Public
Forked from MetaRocq/metarocqMetaprogramming, verified meta-theory and implementation of Coq in Coq
Coq MIT License UpdatedJun 12, 2024 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Coq Other UpdatedJun 8, 2024 -
coq-library-undecidability Public
Forked from uds-psl/coq-library-undecidabilityA library of mechanised undecidability proofs in the Coq proof assistant.
Coq Mozilla Public License 2.0 UpdatedJun 8, 2024 -
unicoq Public
Forked from unicoq/unicoqAn enhanced unification algorithm for Coq
OCaml MIT License UpdatedJun 4, 2024 -
rewriter Public
Forked from mit-plv/rewriterReflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq Other UpdatedJun 3, 2024 -
coq-serapi Public
Forked from rocq-archive/coq-serapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
OCaml Other UpdatedJun 3, 2024 -
coqhammer Public
Forked from lukaszcz/coqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
OCaml Other UpdatedJun 2, 2024 -
coq-waterproof Public
Forked from impermeable/coq-waterproofCoq GNU Lesser General Public License v3.0 UpdatedApr 2, 2024 -
coq-lean-import Public
Forked from rocq-community/rocq-lean-importOCaml GNU Lesser General Public License v2.1 UpdatedApr 2, 2024 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedApr 2, 2024 -
-
coq-opam Public
Forked from rocq-prover/opamArchive for all Coq related OPAM packages organized in various repositories
OCaml GNU Lesser General Public License v2.1 UpdatedDec 7, 2023 -
{{ message }}