summaryrefslogtreecommitdiff
path: root/BFF.agda
diff options
context:
space:
mode:
Diffstat (limited to 'BFF.agda')
-rw-r--r--BFF.agda4
1 files changed, 2 insertions, 2 deletions
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