"Equiv" should have "Mode !"
The Equiv
class should definitely have Hint Mode !
. This used to be blocked on https://github.com/coq/coq/issues/14441; we should probably test if now that the issue is resolved, this actually works as expected.
The fix landed in Coq 8.15, so it will anyway be a while until we can really use this in std++.