[ fix #2153 ] Properly re-export specialised combinators (#2161)

Author: gallais

CHANGELOG.md

@@ -33,6 +33,9 @@ Bug-fixes
   in `Function.Construct.Composition` had their arguments in the wrong order. They have
   been flipped so they can actually be used as a composition operator.
 
+* The operations `_∷=_` and `_─_` exported from `Data.List.Membership.Setoid` 
+  had an extraneous `{A : Set a}` parameter. This has been removed.
+
 * The combinators `_≃⟨_⟩_` and `_≃˘⟨_⟩_` in `Data.Rational.Properties.≤-Reasoning`
   now correctly accepts proofs of type `_≃_` instead of the previous proofs of type `_≡_`.
 

src/Data/List/Membership/Setoid.agda

@@ -13,7 +13,7 @@ module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Function.Base using (_∘_; id; flip)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
-open import Data.List.Relation.Unary.Any
+open import Data.List.Relation.Unary.Any as Any
   using (Any; index; map; here; there)
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
@@ -35,7 +35,8 @@ x ∉ xs = ¬ x ∈ xs
 ------------------------------------------------------------------------
 -- Operations
 
-open Data.List.Relation.Unary.Any using (_∷=_; _─_) public
+_∷=_ = Any._∷=_ {A = A}
+_─_ = Any._─_ {A = A}
 
 mapWith∈ : ∀ {b} {B : Set b}
            (xs : List A) → (∀ {x} → x ∈ xs → B) → List B