Skip to content

Enable `Typeclasses Strict Resolution` for dervied_connectives.v

Janno requested to merge ci/janno/strict-tc-resolution into master

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 Modes, 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.

Merge request reports