From ce6f4e191347aa689de4248ac3a2f9babccf4469 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 27 Jun 2021 19:05:55 +0000
Subject: [PATCH] fix spacing

---
 iris/bi/big_op.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 0ba0adb94..600b0c285 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 _). }
-- 
GitLab