From 316d67c3be31dfa478cf59ba394e520a480753ac Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 28 Jan 2018 18:18:25 -0500
Subject: [PATCH] fix(library/init/data/setoid): fix redundant parameter

`setoid.refl` has two instances of `setoid A` in it
---
 library/init/data/setoid.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/library/init/data/setoid.lean b/library/init/data/setoid.lean
index f5bcbc1487..be744475a3 100644
--- a/library/init/data/setoid.lean
+++ b/library/init/data/setoid.lean
@@ -14,11 +14,9 @@ instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α :=
 ⟨setoid.r⟩
 
 namespace setoid
-variable {α : Sort u}
-variable [s : setoid α]
-include s
+variables {α : Sort u} [setoid α]
 
-@[refl] lemma refl [setoid α] (a : α) : a ≈ a :=
+@[refl] lemma refl (a : α) : a ≈ a :=
 match setoid.iseqv α with
 | ⟨h_refl, h_symm, h_trans⟩ := h_refl a
 end