Pierre-Marie Pédrot (Jun 16 2020 at 12:34): 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?
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
Pierre-Marie Pédrot (Jun 16 2020 at 12:34):then we drop the result
Pierre-Marie Pédrot (Jun 16 2020 at 12:34):and call simple apply with the original term
Pierre-Marie Pédrot (Jun 16 2020 at 12:35):@Matthieu Sozeau maybe?
Pierre-Marie Pédrot (Jun 16 2020 at 12:36):neither auto nor typeclasses eauto do that
Matthieu Sozeau (Jun 16 2020 at 13:30):I don't know why it would do that.
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?
Pierre-Marie Pédrot (Jun 19 2020 at 13:35):the semantics of eauto doesn't correspond to the documentation
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
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
Pierre-Marie Pédrot (Jun 19 2020 at 13:36):... except that if this is the intended semantics, then it's buggy
Pierre-Marie Pédrot (Jun 19 2020 at 13:37):because sometimes it mixes 'old' evars with 'new' ones
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: Jun 04 2023 at 19:30 UTC