diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 4b27896974f6c4ff389ee59231d090c46e344db3..bd69ec9a8bb60f1adc8a694ac6a895674102b2d4 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -637,6 +637,9 @@ Global Instance exclusive_id_free x : Exclusive x → IdFree x.
 Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
 Global Hint Extern 0 (?a ≼ ?a ⋅ _) => apply: cmra_included_l : core.
 Global Hint Extern 0 (?a ≼ _ ⋅ ?a) => apply: cmra_included_r : core.
 
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 47b946117291e9ffd323af9745ac527e552590e8..3a76de3544392250902d61d410b9c73cffa08163 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -369,7 +369,10 @@ Proof.
 Qed.
 End cmra.
 
-Global Hint Extern 4 (_ ≼ CsumBot) => apply: CsumBot_included : core.
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ CsumBot) => apply: CsumBot_included : core.
 Global Arguments csumR : clear implicits.
 
 (* Functor *)
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 7ffff44b84966998972e903b6a01eabaf47ad604..94b792756e991b665a3763e37f36233dc524f54a 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -116,7 +116,10 @@ Lemma ExclBot_included ea : ea ≼ ExclBot.
 Proof. by exists ExclBot. Qed.
 End excl.
 
-Global Hint Extern 4 (_ ≼ ExclBot) => apply: ExclBot_included : core.
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ ExclBot) => apply: ExclBot_included : core.
 
 Global Arguments exclO : clear implicits.
 Global Arguments exclR : clear implicits.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 5041d5690791cf62c25eebfae9bcbe3b9d8d6192..6a7eca83d87be6eaeb683abc65814efb5a6cb835 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -159,8 +159,7 @@ Section internal_eq_derived.
   Qed.
 
   Lemma csum_equivI {A B : ofe} (sx sy : csum A B) :
-    sx ≡ sy ⊣⊢
-              match sx, sy with
+    sx ≡ sy ⊣⊢ match sx, sy with
                | Cinl x, Cinl y => x ≡ y
                | Cinr x, Cinr y => x ≡ y
                | CsumBot, CsumBot => True
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index 85b9abdc7d58ee26bdb8db7b5df2bc0e2ec2f899..f3a8b9a20f46e2d9f19823c2242b48da1a74daed 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -57,7 +57,7 @@ Section internal_included_laws.
 
   Lemma internal_included_refl `{!CmraTotal A} (x : A) : ⊢@{PROP} x ≼ x.
   Proof. iExists (core x). by rewrite cmra_core_r. Qed.
-  Lemma internal_included_trans `{!CmraTotal A} (x y z : A) :
+  Lemma internal_included_trans {A} (x y z : A) :
     ⊢@{PROP} x ≼ y -∗ y ≼ z -∗ x ≼ z.
   Proof.
     iIntros "#[%x' Hx'] #[%y' Hy']". iExists (x' â‹… y').