Pinned Repositories
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
algebra
Basics notions of algebra
analysis
Mathematical Components compliant Analysis Library
argosy
Proving crash safety for systems with layered recovery
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
coq-hh
Hugo Herbelin's public Coq branches
cours-preuves-ordinateur
Page du cours preuves assistées par ordinateur 2021
LMFI-HoTT
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
herbelin's Repositories
herbelin/coq-hh
Hugo Herbelin's public Coq branches
herbelin/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
herbelin/algebra
Basics notions of algebra
herbelin/color
Coq library on rewriting theory and termination
herbelin/coq-ext-lib
A library of Coq definitions, theorems, and tactics.
herbelin/coqprime
Prime numbers for Coq
herbelin/Encyclopedia
An Open Encyclopedia of Proof Systems
herbelin/fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography.
herbelin/iris-coq
The Coq development for Iris (mirrored)
herbelin/ltac2
A standalone implementation of Ltac2 as a Coq plugin
herbelin/ocaml
The core OCaml system: compilers, runtime system, base libraries
herbelin/opam
opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.
herbelin/plugin_tutorials
A collection of small projects to illustrate how to write plugins for Coq
herbelin/qarith-stern-brocot
Binary Rational Numbers [maintainer=@herbelin]
herbelin/topology
Formal topology (and some probability) in Coq
herbelin/zorns-lemma
This library develops some basic set theory [maintainer=@amiloradovsky]