Does anybody know why we do the unification work twice in Eauto.unify_e_resolve?
we first call clenv_unique_resolver, which will unify the conclusion with the type of the clenv
then we drop the result
and call simple apply with the original term
@Matthieu Sozeau maybe?
neither auto nor typeclasses eauto do that
I don't know why it would do that.
@Matthieu Sozeau could you comment on my last comment in https://github.com/coq/coq/pull/12532?
the semantics of eauto doesn't correspond to the documentation
it claims it uses simple eapply, and the latter is not allowed to perform conversion on non-ground terms but it's not true
it seems to be allowed to do so when the evar was preexistent to the eauto invocation
... except that if this is the intended semantics, then it's buggy
because sometimes it mixes 'old' evars with 'new' ones
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