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.
Last updated: Oct 16 2021 at 01:03 UTC