fix compilation with agda 2.5.3, agda-stdlib 0.14

3 files changed, 5 insertions, 4 deletions

diff --git a/Examples.agda b/Examples.agda
index cfe9432..bedad5a 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -2,7 +2,7 @@ module Examples where
 
 open import Data.Maybe using (just ; nothing)
 open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉)
-open import Data.Nat.Properties using (cancel-+-left)
+open import Data.Nat.Properties using (cancel-+-left ; ≤-decTotalOrder)
 import Algebra.Structures
 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map)
@@ -19,7 +19,7 @@ open GetTypes.PartialVecVec using (Get)
 open FreeTheorems.PartialVecVec using (assume-get)
 open BFF.PartialVecBFF using (bff)
 
-ℕ-decSetoid = Relation.Binary.DecTotalOrder.Eq.decSetoid Data.Nat.decTotalOrder
+ℕ-decSetoid = Relation.Binary.DecTotalOrder.Eq.decSetoid ≤-decTotalOrder
 
 reverse' : Get
 reverse' = assume-get id id reverse
diff --git a/FinMap.agda b/FinMap.agda
index ca7e73b..3786b97 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -11,6 +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
 open import Function using (id ; _∘_ ; flip ; const)
 open import Function.Equality using (module Π)
 open import Function.Surjection using (module Surjection)
@@ -23,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 = Any.Membership._∈_ (P.setoid A) x (toList xs)
+_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs)
 
 _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
 _∉_ {A} x xs = All (_≢_ x) (toList xs)
diff --git a/Precond.agda b/Precond.agda
index 70f294d..cc81db4 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -16,7 +16,7 @@ open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
 open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
 import Data.List.All
 open import Data.List.Any using (here ; there)
-open Data.List.Any.Membership-≡ using (_∉_)
+open import Data.List.Any.Membership.Propositional using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)