From 62966bac293b2f2b1e142b462923e74d8a951e56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Aug 2019 18:37:51 +0200
Subject: [PATCH] Remove useless space.

---
 theories/list.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/list.v b/theories/list.v
index dc522408..c53e23b6 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3677,7 +3677,7 @@ Section zip_with.
     zip_with f l (k1 ++ k2)
     = zip_with f (take (length k1) l) k1 ++ zip_with f (drop (length k1) l) k2.
   Proof. revert l. induction k1; intros [|??]; f_equal/=; auto. Qed.
-  Lemma zip_with_flip l k : zip_with (flip f) k l =  zip_with f l k.
+  Lemma zip_with_flip l k : zip_with (flip f) k l = zip_with f l k.
   Proof. revert k. induction l; intros [|??]; f_equal/=; auto. Qed.
   Lemma zip_with_ext (g : A → B → C) l1 l2 k1 k2 :
     (∀ x y, f x y = g x y) → l1 = l2 → k1 = k2 →
-- 
GitLab