port to agda/2.5.4.1 and agda-stdlib/0.17

1 files changed, 2 insertions, 2 deletions

diff --git a/FinMap.agda b/FinMap.agda
index 7380b71..df422c3 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -11,7 +11,7 @@ open import Data.Product using (_×_ ; _,_)
 open import Data.List.All as All using (All)
 import Data.List.All.Properties as AllP
 import Data.List.Any as Any
-import Data.List.Any.Membership.Propositional
+import Data.List.Membership.Setoid
 open import Function using (id ; _∘_ ; flip ; const)
 open import Function.Equality using (module Π)
 open import Function.Surjection using (module Surjection)
@@ -24,7 +24,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Generic using (just-injective)
 
 _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
-_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs)
+_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs)
 
 _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
 _∉_ {A} x xs = All (_≢_ x) (toList xs)