From b73292939343615f5e60af132aa901563030a154 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 17 Oct 2023 13:06:15 +0100
Subject: [PATCH 1/2] [ fix #2153 ] Properly re-export specialised combinators

---
 src/Data/List/Membership/Setoid.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 1b8a67fb7d..1a19169992 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/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

From fa6cde55dbde5b05e301ba99a64b239a32a1751b Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 19 Oct 2023 09:47:51 +0900
Subject: [PATCH 2/2] Add CHANGELOG entry

---
 CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89e22ce60e..b4b91488f7 100644
--- a/CHANGELOG.md
+++ b/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 `_≡_`.