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

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

(limited to 'BFF.agda')

diff --git a/BFF.agda b/BFF.agda
index 79f3b3d..ddf2307 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -16,10 +16,10 @@ open import Relation.Binary using (DecSetoid ; module DecSetoid)
 open import FinMap
 open import Generic using (mapMV)
 import CheckInsert
-import FreeTheorems
+import GetTypes
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open FreeTheorems.VecVec public using (Get)
+  open GetTypes.VecVec public using (Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
-- 
cgit v1.2.3