From e847956f7d044e1ac5bc256aa22a4c07058e132c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jul 2022 12:30:19 -0400
Subject: [PATCH] remove a useless auto

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

diff --git a/theories/list.v b/theories/list.v
index d7024602..b78ba495 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4274,7 +4274,7 @@ Section imap.
   Lemma imap_app l1 l2 :
     imap f (l1 ++ l2) = imap f l1 ++ imap (λ n, f (length l1 + n)) l2.
   Proof.
-    revert f. induction l1 as [|x l1 IH]; intros f; f_equal/=; auto.
+    revert f. induction l1 as [|x l1 IH]; intros f; f_equal/=.
     by rewrite IH.
   Qed.
   Lemma imap_cons x l : imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
-- 
GitLab