-
logrel-coq Public
Forked from CoqHott/logrel-coqLogical Relation for MLTT in Coq
Coq MIT License UpdatedNov 28, 2025 -
-
platform-docs Public
Forked from rocq-prover/platform-docsA project of short tutorials and how-to guides for Coq features and Coq Platform packages.
Rocq Prover Other UpdatedJul 4, 2025 -
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 UpdatedApr 18, 2025 -
rocq Public
Forked from rocq-prover/rocqThe 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…
OCaml GNU Lesser General Public License v2.1 UpdatedApr 16, 2025 -
paramcoq Public
Forked from rocq-community/paramcoqOld Coq plugin for parametricity [maintainer=@ppedrot]
Coq Other UpdatedApr 16, 2025 -
metarocq Public
Forked from MetaRocq/metarocqMetaprogramming, verified meta-theory and implementation of Rocq in Rocq
Coq MIT License UpdatedApr 16, 2025 -
rocq-lean-import Public
Forked from rocq-community/rocq-lean-importOCaml GNU Lesser General Public License v2.1 UpdatedApr 16, 2025 -
PiMPvitefait Public
Forked from ppedrot/vitefPiMP's junkyard to stuff bits of quick-n'-dirty code
Coq UpdatedMar 13, 2025 -
{{ message }}