Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available. (!273) · Merge requests · Iris / stdpp

Merged Matthieu Sozeau requested to merge mattam82/stdpp:coq-13969 into master Jun 04, 2021

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

Edited Jul 26, 2021 by Ralf Jung

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