Enable `Typeclasses Strict Resolution` for dervied_connectives.v
Typeclasses Strict Resolution
can be seen as a sane version of Hint Mode +
: instead of outlawing evars altogether, it simply freezes them. Sadly, unlike Hint Mode
, it cannot be set for a single argument. However, the classes in this file have no -
Hint Mode
s, which makes me think that none of them should ever be used to instantiate evars in any argument.
I assume there will be breakage because this Coq feature is unlikely to be thoroughly exercised by anyone.
(This is the same as !641 (closed) which was closed accidentally when I renamed the branch.)
TODO:
-
add comment that explains the semantics of the setting.