From f767ec96fec169907da5cb5029852732cf333e7b Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 28 Jan 2014 09:30:45 +0100
Subject: use the indexed version of the Vec Setoid

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

(limited to 'CheckInsert.agda')

diff --git a/CheckInsert.agda b/CheckInsert.agda
index 47af215..c8007ec 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -18,7 +18,6 @@ import Relation.Binary.EqReasoning as EqR
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
 
 open import FinMap
-open import Generic using (vecIsSetoid)
 
 private
   open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq)
-- 
cgit v1.2.3