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

---
 src/Acknowledgements.lagda | 9 ++++++---
 src/TypedBadfix.lagda      | 4 ++--
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Acknowledgements.lagda b/src/Acknowledgements.lagda
index e3527853..2b68f38b 100644
--- a/src/Acknowledgements.lagda
+++ b/src/Acknowledgements.lagda
@@ -17,13 +17,15 @@ To Andreas Abel and Ulf Norell, ditto.
 To David Darais, for showing me how much more compact it is to avoid raw terms.
 
 For pull requests.
-* Jonathan Prieto-Cubides
 * Vikraman Choudhury
-* Anish Tondwalkar 
+* Phil de Joux
+* koo5
+* Juhana Laurinharju
+* Jonathan Prieto-Cubides
+* Anish Tondwalkar
 
 For answering questions on the Agda mailing list.
 * Guillaume Allais <guillaume.allais@ens-lyon.org>
-* Sabry, Amr A. <sabry@indiana.edu>
 * Nils Anders Danielsson <nad@cse.gu.se>
 * Miëtek Bak <mietek@bak.io>
 * Gergő Érdi <gergo@erdi.hu>
@@ -34,6 +36,7 @@ For answering questions on the Agda mailing list.
 * Liam O'Connor <liamoc@cse.unsw.edu.au>
 * N. Raghavendra <nyraghu27132@gmail.com>
 * Roman <effectfully@gmail.com>
+* Amr A. Sabry <sabry@indiana.edu>
 
 For comments on the text.
 * [your name goes here]
diff --git a/src/TypedBadfix.lagda b/src/TypedBadfix.lagda
index 146c21ed..f1847a36 100644
--- a/src/TypedBadfix.lagda
+++ b/src/TypedBadfix.lagda
@@ -29,7 +29,7 @@ open import Function.Equivalence using (_⇔_; equivalence)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (contraposition; ¬?)
 open import Relation.Nullary.Product using (_×-dec_)
-open import Collections using (_↔_)
+import Collections
 \end{code}
 
 
@@ -219,7 +219,7 @@ erase-lemma (⊢L · ⊢M)         =  cong₂ _·_ (erase-lemma ⊢L) (erase-lem
 ### Lists as sets
 
 \begin{code}
-open Collections.CollectionDec (Id) (_≟_)
+open Collections (Id) (_≟_)
 \end{code}
 
 ### Free variables