Std++ 1.3

Dear Coq discourse,

we are pleased to announce the release of std++ 1.3: an extended “standard” library for Coq. The std++ library includes a large selection of definitions and lemmas on common data structures like lists, relations, sets, finite sets, finite maps, and finite multisets; a number of type classes for common properties of types (e.g., decidable equality, countable, finite, infinite, inhabited); and useful tactics.

This release of the std++ library adds support for Coq 8.11 and is available in Coq’s opam repository.

The changelog for this release can be found at

This release of std++ received contributions by Amin Timany, Armaël Guéneau, Dan Frumin, David Swasey, Jacques-Henri Jourdan, Michael Sammler, Paolo G. Giarrusso, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Tej Chajed, and William Mansky.

More information is available at


The std++ team