diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 5a5d2ca4a644198c67cd0575848bacca4cbf50db..51b05327302c1c7aa9dc21f82c157284e3ead109 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 7900d9db784d7e258c386680126bd6151d817ca0..c5a73d5595094314d983b8d89c9d1b8ebc662caa 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 :