CoHTTP implementation using the Lwt concurrency library (dev)

CoHTTP implementation for Unix and Windows using Lwt (runtime)

CoHTTP implementation for Unix and Windows using Lwt (dev)

OCaml library for HTTP clients and servers (runtime)

OCaml library for HTTP clients and servers (dev)

OCaml compiler library (development files)

network connection establishment library for Lwt (runtime)

network connection establishment library for Lwt (dev)

network connection establishment library for OCaml (runtime)

network connection establishment library for OCaml (dev)

OCaml library for managing configuration files (dev files)

Coq library for big numbers

algebra and data structure algorithms for Coq

Primality certification for Coq (library)

Coq library for real analysis

runtime libraries for Coq

development libraries and tools for Coq

Coq Constructive Repository at Nijmegen

deriving MathComp classes from inductive types

Coq plugin to extract dependencies between Coq objects

Coq plugin embedding Elpi

Coq library to work with functions defined by equations

Collection of theories and plugins for Coq

data structures with extensional reasoning for Coq

Floating-point arithmetic for Coq

automated reasoning tool for Coq

build hierarchies of algebraic structures in Coq

Coq library for homotopy type theory

interval arithmetic for Coq

high-order concurrent separation logic framework for Coq

Tactics on hypotheses in Coq

Abstract interfaces for mathematical structures for Coq

Ring and field tactics for Mathematical Components

analysis extension for Mathematical Components

epsilon - N reasoning for Mathematical Components

classical logic extension for Mathematical Components

finite sets and maps extension for Mathematical Components

Multivariate polynomials for Mathematical Components

Real closed fields for Mathematical Components

Micromega arithmetic solvers for Mathematical Components

support library for Coq-verified Menhir parsers

Mtac2 tactic language for Coq

Ott tool (Coq plugin)

Coq plugin to generate parametricity statements

randomized testing framework for Coq (plugin)

automatic record fields updaters for Coq

reduction effects for Coq

representation of regular languages in Coq

relation algebra for Coq

interaction with Coq (runtime)