Stream: Coq devs & plugin devs

Topic: typeclasses eauto vs simple eapply


view this post on Zulip 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?

view this post on Zulip Jason Gross (Oct 22 2020 at 01:38):

Reported as https://github.com/coq/coq/issues/13239

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 08:26):

No, it's yet another set of flags if I read correctly.


Last updated: Oct 16 2021 at 01:03 UTC