diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 6139e4088723542fec3cfc38f1f56ed3dc6425cd..b41c31efc438c05a3b1de815856d2a931702a3ad 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -82,6 +82,7 @@ Section lemmas.
   (* higher cost than the Fractional instance, which is used for a1 = a2 *)
   Proof.
     rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
+    (* FIXME: in the future a single [iCombine] should suffice here. *)
     iCombine "H1 H2" gives %[_ ->].
     by iCombine "H1 H2" as "H".
   Qed.