Bidirectional hints change program obligation order in unexpected ways

[Janno]

Description of the problem

I probably would not be as surprised by a change in obligation order if the & was not before all arguments but somewhere in the middle. Even then, I think it would be much better if the order was stable.

I have a branch that orders obligations by their original evar id (inherited when one evar replaces another) which fixes this particular example. Is that a sensible way to go about it? If so, I'll open a PR.

Small Rocq / Coq file to reproduce the bug

Axiom P Q : Prop.
Axiom f : P -> nat.
Axiom g : Q -> nat.

Record R := {
  op1 : nat;
  op2 : nat;
  law : op1 = op1
}.

Axiom H1 : P.
Axiom H2 : Q.

Local Obligation Tactic := idtac.
Program Definition r : R := {|
  op1 := f _;
  op2 := g _
|}.
(* Obligations are in argument order *)
Next Obligation. apply H1. Qed.
Next Obligation. apply H2. Qed.
Next Obligation. reflexivity. Qed.

Arguments Build_R & _ _ _.

Local Obligation Tactic := idtac.
Program Definition r' : R := {|
  op1 := f _;
  op2 := g _
|}.
(* Obligations are no longer in argument order *)
Next Obligation. apply H1. Qed.
Next Obligation. reflexivity. Qed.
Next Obligation. apply H2. Qed.

Version of Rocq / Coq where this bug occurs

8.16, 9.2

Interface of Rocq / Coq where this bug occurs

No response

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

No response