From 1286deef698a9fbf92b86d0078fd62c47f980ee9 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sat, 1 Aug 2020 09:12:17 +0200
Subject: move imports for agda-stdlib 1.3

---
 CheckInsert.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CheckInsert.agda')

diff --git a/CheckInsert.agda b/CheckInsert.agda
index dbba6e6..68f5fdb 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -13,7 +13,7 @@ open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
-import Relation.Binary.EqReasoning as EqR
+import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning)
 
 open import FinMap
-- 
cgit v1.2.3