Andrej Dudenhefner

The reason for the arbitrary behavior is that `auto` currently uses three different unification procedures for 1) hypotheses with zero arguments 2) hints with zero arguments 3) hypotheses or hints...

For the record, `ssreflect`'s `apply: transport_forall_constant.` does work (also with underscores) in the initial example. (Coq 8.16+rc1).

The debug logs are: ``` typeclasses eauto with nocore 1: looking for (forall P : unit -> Prop, P (id tt) -> P tt) without backtracking 1: no match for...

> It seems to be because I'm not sure about this. The following also fails: `typeclasses eauto with core`. So the underlying issues is also orthogonal from the `with` clause.

I see. Also we have `Succeed (typeclasses eauto with empty).`.

Currently (Coq 8.16) for `auto` we have that - `Extern` hints use `Constr_matching.matches` (without flags) to match the pattern with the goal - `Resolve` hints use `Unification.w_unify` (with flags) to...

@xavierleroy I did check that this PR compiles both before and after https://github.com/coq/coq/pull/16293. The main reason for the proposed changes is that fixing bugs in `auto` may allow it to...

> I don't think this solves the linked bug, because there are still discrepancies between (e)auto and simple (e)apply. At least, regarding the linked bug, the following works as expected:...

The bench shows that setting `use_metas_eagerly_in_conv_on_closed_terms = true` does not lead to major slowdowns. However, much of the ci breaks because of the anti-pattern: `tac1; auto. tac2`. Since `(e)auto` became...

> "solve all the side-conditions arising from the rewrite, but do _not_ try to solve the main goal, and error if any side-condition fails to solve" -- something that reliably...