From fef9016bd3ca6544f0110bdbf8dbe6ca24120450 Mon Sep 17 00:00:00 2001
From: Oliver Nash
Date: Tue, 3 Sep 2019 20:38:16 +0100
Subject: Remove redundant parameter in List.concat_filter_map

---
 theories/Lists/List.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f45317ba50..88c47b9744 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1234,11 +1234,11 @@ End Fold_Right_Recursor.
       destruct (f x); simpl; now rewrite IH.
     Qed.
 
-    Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool),
+    Lemma concat_filter_map : forall (l : list (list A)),
       concat (map filter l) = filter (concat l).
     Proof.
       induction l as [| v l IHl]; [auto|].
-      simpl. rewrite (IHl f). rewrite filter_app. reflexivity.
+      simpl. rewrite IHl. rewrite filter_app. reflexivity.
     Qed.
 
   (** [find] *)
-- 
cgit v1.2.3