Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12

Includes fixes for Coq 8.12/8.13 — but we might want to drop those.

Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of those annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:

 (* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
 fixed in Coq >= 8.12, which Iris depends on. *)

stdpp/base.v

@@ -267,11 +267,10 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
-(* No Hint Mode set because of Coq bug #14441.
-Global Hint Mode Equiv ! : typeclass_instances. *)
+Global Hint Mode Equiv ! : typeclass_instances.
 
-(** We instruct setoid rewriting to infer [equiv] as a relation on 
-type [A] when needed. This allows setoid_rewrite to solve constraints 
+(** We instruct setoid rewriting to infer [equiv] as a relation on
+type [A] when needed. This allows setoid_rewrite to solve constraints
 of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
 when an equivalence relation is available on type [A]. We put this instance
 at level 150 so it does not take precedence over Coq's stdlib instances,