From 19670abeff9895de593ef26ad2da247ae590ce90 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Thu, 30 Jan 2014 09:13:11 +0100
Subject: allow importing of Bidir without any postulates

---
 Bidir.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 42f8821..e792b3a 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -24,8 +24,8 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ;
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
-import FreeTheorems
-open FreeTheorems.VecVec using (Get ; module Get)
+import GetTypes
+open GetTypes.VecVec using (Get ; module Get)
 open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
 open import FinMap
 import CheckInsert
-- 
cgit v1.2.3