Make backwards compatible.

iris/algebra/gmap.v

@@ -113,7 +113,7 @@ Global Arguments gmapO _ {_ _} _.
 (** Non-expansiveness of higher-order map functions and big-ops *)
 Global Instance merge_ne `{Countable K} {A B C : ofe} n :
   Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
-          dist n ==> dist n ==> dist n) (merge (MA:=gmap K A)).
+          dist n ==> dist n ==> (≡{n}@{gmap K C}≡)) merge.
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
@@ -126,7 +126,8 @@ Proof.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
 Global Instance map_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (MA:=gmap K A) f).
+  Proper (dist n ==> dist n) f →
+  Proper (dist n ==> (≡{n}@{gmap K B}≡)) (fmap f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
 Global Instance map_zip_with_ne `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
@@ -713,9 +714,6 @@ Qed.
 End unital_properties.
 
 (** Functor *)
-Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (MA:=gmap K A) f).
-Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
 Lemma gmap_fmap_ne_ext `{Countable K}
   {A : Type} {B : ofe} (f1 f2 : A → B) (m : gmap K A) n :
   (∀ i x, m !! i = Some x → f1 x ≡{n}≡ f2 x) →

iris/algebra/list.v

@@ -125,10 +125,10 @@ Global Arguments listO : clear implicits.
 
 (** Non-expansiveness of higher-order list functions and big-ops *)
 Global Instance list_fmap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (fmap (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) fmap.
 Proof. intros f1 f2 Hf l1 l2 Hl; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Global Instance list_omap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (omap (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) omap.
 Proof.
   intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
   destruct (Hf _ _ Hx); [f_equiv|]; auto.
@@ -142,10 +142,10 @@ Proof.
   f_equiv; [by apply Hf|]. apply IH. intros i y1 y2 Hy. by apply Hf.
 Qed.
 Global Instance list_bind_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n)
-         (mbind (A:=A) (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list B}≡) ==> (≡{n}@{list A}≡)) mbind.
 Proof. intros f1 f2 Hf. induction 1; csimpl; [constructor|f_equiv; auto]. Qed.
-Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (MA:=list A)).
+Global Instance list_join_ne {A : ofe} n :
+  Proper (dist n ==> (≡{n}@{list A}≡)) mjoin.
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
 Global Instance zip_with_ne {A B C : ofe} n :
   Proper ((dist n ==> dist n ==> dist n) ==> dist n ==> dist n ==> dist n)

iris/algebra/ofe.v

@@ -1295,13 +1295,13 @@ Global Typeclasses Opaque option_dist.
 Global Arguments optionO : clear implicits.
 
 Global Instance option_fmap_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap A B (option A) (option B) _).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) fmap.
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
 Global Instance option_mbind_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind A (option A) (option B) _).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) mbind.
 Proof. destruct 2; simpl; auto. Qed.
 Global Instance option_mjoin_ne {A : ofe} n:
-  Proper (dist n ==> dist n) (@mjoin (option A) (option (option A)) _).
+  Proper (dist n ==> (≡{n}@{option A}≡)) mjoin.
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
 Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :

iris_unstable/heap_lang/interpreter.v

@@ -151,7 +151,7 @@ Module interp_monad.
   Proof. by inversion 1. Qed.
 
   Lemma mret_inv {A} (v: A) s v' s' :
-    mret (MA:=InterpretM A) v s = (inl v', s') → v = v' ∧ s = s'.
+    (mret v : InterpretM A) s = (inl v', s') → v = v' ∧ s = s'.
   Proof. by inversion 1. Qed.
 
   Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
@@ -176,7 +176,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
-    (fmap (MA:=InterpretM A) f x) s = (inl v, s') →
+    (fmap f x : InterpretM B) s = (inl v, s') →
     ∃ v0, v = f v0 ∧ x s = (inl v0, s').
   Proof.
     rewrite /fmap /interp_fmap.
@@ -240,7 +240,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inr_inv {A B} (f: A → B) (x: InterpretM A) s e s' :
-    (fmap (MB := InterpretM B) f x) s = (inr e, s') →
+    (fmap f x : InterpretM B) s = (inr e, s') →
     x s = (inr e, s').
   Proof.
     rewrite /fmap /interp_fmap.

tests/algebra.v

@@ -92,5 +92,5 @@ Proof. apply _. Qed.
 
 (** Regression test for https://gitlab.mpi-sws.org/iris/iris/-/issues/577 *)
 Lemma list_bind_ne_test {A B : ofe} (f : A → list B) :
-  NonExpansive f → NonExpansive (mbind (MA:=list A) f).
+  NonExpansive f → NonExpansive (mbind f : list A → list B).
 Proof. apply _. Qed.