From 2e0bf441c68c8a96c460c55402d0a25635fafa0e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Jul 2019 12:07:16 +0200
Subject: [PATCH] name fmap_inj

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

diff --git a/theories/list.v b/theories/list.v
index abadc41f..19023309 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3100,7 +3100,7 @@ Section fmap.
     (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
   Proof. induction l; constructor; auto. Qed.
 
-  Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
+  Global Instance fmap_inj: Inj (=) (=) f → Inj (=) (=) (fmap f).
   Proof.
     intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
     intros [|??]; intros; f_equal/=; simplify_eq; auto.
-- 
GitLab