From ec91c14fec83e5f61848432d893f9d25742d76dc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jan 2020 22:49:24 +0100
Subject: [PATCH] Strengten `fmap_equiv_ext` lemmas.

The `Equiv` instance for the domain is not needed.
---
 theories/fin_maps.v | 2 +-
 theories/option.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 5a5d2ca4..51b05327 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -643,7 +643,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
   g ∘ f <$> m = g <$> (f <$> m).
 Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
-Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) (m : M A) :
+Lemma map_fmap_equiv_ext {A} `{Equiv B} (f1 f2 : A → B) (m : M A) :
   (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
 Proof.
   intros Hi i; rewrite !lookup_fmap.
diff --git a/theories/option.v b/theories/option.v
index 7900d9db..c5a73d55 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -209,7 +209,7 @@ Proof. by destruct mx. Qed.
 Lemma option_fmap_ext {A B} (f g : A → B) mx :
   (∀ x, f x = g x) → f <$> mx = g <$> mx.
 Proof. intros; destruct mx; f_equal/=; auto. Qed.
-Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) (mx : option A) :
+Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A → B) (mx : option A) :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
-- 
GitLab