Jason Gross (Oct 22 2020 at 01:29): Jason Gross (Oct 22 2020 at 01:29):I think I found a case where typeclasses eauto behavior differs from simple eapply. Is this expected?
Jason Gross (Oct 22 2020 at 01:38):Reported as https://github.com/coq/coq/issues/13239
Maxime Dénès (Oct 22 2020 at 07:47):https://github.com/coq/coq/pull/991 fixes some such discrepancies, maybe you can try your example on the branch?
Théo Zimmermann (Oct 22 2020 at 08:19):@Jason Gross In practice, I believe that typeclasses eauto uses autoapply rather than simple eapply, despite what the log says.
Pierre-Marie Pédrot (Oct 22 2020 at 08:26):No, it's yet another set of flags if I read correctly.
Jason Gross (Nov 01 2022 at 00:55):Is there a version of autoapply that does not shelve dependent typeclass subgoals?
Last updated: Oct 08 2024 at 15:02 UTC