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: Jun 08 2023 at 04:01 UTC