From 1cddc512210d5e96ffa9b7bd5282ff2c4beee516 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 9 May 2018 19:45:15 -0300
Subject: [PATCH] fixed imports of Collections

---
 src/TypedBarendregt.lagda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/TypedBarendregt.lagda b/src/TypedBarendregt.lagda
index 0ac63bae..414b9b84 100644
--- a/src/TypedBarendregt.lagda
+++ b/src/TypedBarendregt.lagda
@@ -33,7 +33,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Function using (_∘_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (¬?)
-open import Collections
+import Collections
 
 pattern [_]     x      =  x ∷ []
 pattern [_,_]   x y    =  x ∷ y ∷ []
@@ -276,7 +276,7 @@ erase-lemma (⊢Y ⊢M)          =  cong `Y_ (erase-lemma ⊢M)
 ### Lists as sets
 
 \begin{code}
-open Collections.CollectionDec (Id) (_≟_)
+open Collections (Id) (_≟_)
 \end{code}
 
 ### Free variables