Opaque foo indeed subsume
Typeclasses Opaque foo , as you’d expect?
I’m revising this code:
Global Typeclasses Opaque foo. Global Opaque foo.
If I swap these statements,
Typeclasses Opaque gives “Cannot coerce to_subst to an evaluable reference.”
For “Ideal Coq”, that means
Typeclasses Opaque is redundant, but I’ve learned we don’t have that yet, so it’d be good to know for sure. Docs for either
Typeclasses Opaque and
Hint Opaque say little except document that
Opaque isn’t really opaque:
Opaque has also an effect on the conversion algorithm of Coq, telling it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section Conversion rules) of two distinct applied constants.
We also have a couple of issues on
Opaque, which is why I’m especially uncertain.