eassumption does not try reduction when unifying

[yannl35133]

Description of the problem

According to the manual,

Behaves like assumption but is able to process goals and hypotheses with existential variables.

Yet assumption has no issues reducing (even eassumption can reduce, but only when the hypothesis' type and the goals have no evars).

Small Rocq / Coq file to reproduce the bug

Goal forall (H : (fun _ => 2=1) 0), exists n, n = 1.
  intros H.
  eexists.
  eassumption.
Abort.

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

Apparently this is deliberate

rocq/tactics/auto.ml

Line 47 in 3595d98

modulo_betaiota = false;