Backward compatible fix for Coq PR#7916

iris/algebra/ofe.v

@@ -13,6 +13,8 @@ Set Primitive Projections.
 
 (** Unbundled version *)
 Class Dist A := dist : nat → relation A.
+Global Instance dist_rewrite {A} (d : Dist A) x : RewriteRelation (dist x) := {}.
+Global Hint Mode RewriteRelation - - : typeclass_instances.
 Global Instance: Params (@dist) 3 := {}.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
@@ -653,9 +655,9 @@ End empty.
 Section product.
   Context {A B : ofe}.
 
+  Typeclasses Transparent dist.
   Local Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
-  Global Instance pair_ne :
-    NonExpansive2 (@pair A B) := _.
+  Global Instance pair_ne : NonExpansive2 (@pair A B) := _.
   Global Instance fst_ne : NonExpansive (@fst A B) := _.
   Global Instance snd_ne : NonExpansive (@snd A B) := _.
   Definition prod_ofe_mixin : OfeMixin (A * B).