std++ 1.2

we are pleased to announce the release of std++ 1.2: 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.

The std++ library is available in Coq’s opam repository.

The changelog for this release can be found at

This release of std++ received contributions by Dan Frumin, Hai Dang, Jan-Oliver Kaiser, Mackie Loeffel, Maxime Dénès, Ralf Jung, Robbert Krebbers, and Tej Chajed.

More information is available at


Will there be a release of Iris compatible with std++ 1.2? It seems that Iris 3.1.0 is not compatible with std++ 1.2.

Thank you.

1 Like

Probably not anytime soon. We would like to write documentation for the changes in Iris ( and that may take a while.

However, the current Iris development version is compatible with std++ 1.2.