diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 4af018de3c71ef4978c632f70f2f91e3de1f6169..1d6337816ca6b3234e34a8b677f88fcf1716b9d1 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -240,7 +240,7 @@ Proof.
   - by split; simpl; rewrite ?cmra_core_l.
   - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
+    by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
     intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 94789d0f170aae332f9cb5d943199f37f5cbdf24..6285c2ab0493ac21efb46d09dac30205f8702d0b 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -165,7 +165,7 @@ Proof.
   - split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
   - split; simpl; [by rewrite cmra_core_idemp|done].
   - intros ??; rewrite! namespace_map_included; intros [??].
-    by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
+    by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
   - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite namespace_map_validN_eq /=.
     rewrite {1}/op /cmra_op /=. case_decide; last done.
     intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.