Stream: Coq devs & plugin devs

Topic: eauto unification


view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:34):

Does anybody know why we do the unification work twice in Eauto.unify_e_resolve?

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:34):

we first call clenv_unique_resolver, which will unify the conclusion with the type of the clenv

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:34):

then we drop the result

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:34):

and call simple apply with the original term

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:35):

@Matthieu Sozeau maybe?

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 12:36):

neither auto nor typeclasses eauto do that

view this post on Zulip Matthieu Sozeau (Jun 16 2020 at 13:30):

I don't know why it would do that.

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:35):

@Matthieu Sozeau could you comment on my last comment in https://github.com/coq/coq/pull/12532?

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:35):

the semantics of eauto doesn't correspond to the documentation

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:36):

it claims it uses simple eapply, and the latter is not allowed to perform conversion on non-ground terms but it's not true

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:36):

it seems to be allowed to do so when the evar was preexistent to the eauto invocation

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:36):

... except that if this is the intended semantics, then it's buggy

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:37):

because sometimes it mixes 'old' evars with 'new' ones

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 13:37):

and arbitrarily decides they shouldn't be allowed in conversion problems even though they come from the outside


Last updated: Oct 16 2021 at 03:02 UTC