I think I found a case where
typeclasses eauto behavior differs from
simple eapply. Is this expected?
Reported as https://github.com/coq/coq/issues/13239
https://github.com/coq/coq/pull/991 fixes some such discrepancies, maybe you can try your example on the branch?
@Jason Gross In practice, I believe that
typeclasses eauto uses
autoapply rather than
simple eapply, despite what the log says.
No, it's yet another set of flags if I read correctly.
Is there a version of
autoapply that does not shelve dependent typeclass subgoals?
Last updated: Feb 01 2023 at 15:04 UTC