diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 0ba0adb942e8df562ea89a10f470ded882dd40c1..600b0c28566c6d03ba74ff78c1afb60be155c02f 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -731,7 +731,7 @@ Section sep_list2.
     intros HΦ. apply (anti_symm _).
     { apply and_intro; [apply big_sepL2_length|].
       apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
-      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepL2_lookup. }
+      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepL2_lookup. }
     apply pure_elim_l=> Hlen.
     revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
     { by apply (affine _). }