Adapt to rocq-prover/rocq#21129.

Author: ppedrot

test-suite/vs.v

@@ -784,7 +784,7 @@ Module M1 : MSetInterface_S_Ext
     (min_elt s = Some k /\ Equal (remove k s) s').
  Proof. intros.
  destruct (remove_min_spec1x s k s') as [? _].
- destruct (H0 H); clear H0 H. split; auto. rewrite H2; intuition.
+ destruct (H0 H); clear H0 H. split; auto. rewrite H2; intuition; auto with *.
  Qed.
  Lemma remove_min_spec2x: forall s, remove_min s = None <-> Empty s.
  Proof. unfold remove_min; intros.