`progress` cannot detect that no progress was done in the presence of defined evars.

[jpoiret]

Description of the problem

If the tactic used with progress yields a new goal that has the same conclusion as the old one, up to an evar, and the evar in the old goal is defined to the evar in the new goal in the new environment.

Small Rocq / Coq file to reproduce the bug

Goal True.
  eassert ?[T].
  (* test when aliasing (thanks to unification) *)
  Fail progress (eassert ?[T'] as H; [|let _ := constr:(eq_refl _ :> ?T = ?T') in exact H]).
  (* test when not aliasing *)
  Fail progress (eassert ?[T'] as H; [|instantiate (T := ?T'); exact H]).
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