Skip to content

Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.

Matthieu Sozeau requested to merge mattam82/stdpp:coq-13969 into master

This makes Iris & Perennial compatible with Coq PR #13969. Should be entirely backwards compatible.

Edited by Ralf Jung

Merge request reports