diff --git a/src/plfa/Acknowledgements.lagda b/acknowledgements.md
similarity index 100%
rename from src/plfa/Acknowledgements.lagda
rename to acknowledgements.md
diff --git a/src/plfa/Inference.lagda b/src/plfa/Inference.lagda
index 27976750..c40055bc 100644
--- a/src/plfa/Inference.lagda
+++ b/src/plfa/Inference.lagda
@@ -250,9 +250,8 @@ We are now ready to begin the formal development.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.String using (String; _≟_)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 \end{code}
diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda
index ca580c81..7c31dea9 100644
--- a/src/plfa/Lambda.lagda
+++ b/src/plfa/Lambda.lagda
@@ -53,8 +53,7 @@ four.
 
 \begin{code}
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Relation.Nullary using (Dec; yes; no; ¬_)
diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda
index 250b7be6..453b96df 100644
--- a/src/plfa/Properties.lagda
+++ b/src/plfa/Properties.lagda
@@ -22,8 +22,7 @@ sequences for us.
 \begin{code}
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym; cong; cong₂)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Product
diff --git a/tspl/Assignment4.lagda b/tspl/Assignment4.lagda
index 6294291d..1251af0b 100644
--- a/tspl/Assignment4.lagda
+++ b/tspl/Assignment4.lagda
@@ -42,8 +42,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 \end{code}
 
diff --git a/tspl/Exam.lagda b/tspl/Exam.lagda
index 4962ae29..78d91936 100644
--- a/tspl/Exam.lagda
+++ b/tspl/Exam.lagda
@@ -25,8 +25,7 @@ open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.List using (List; []; _∷_; _++_)
 open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary using (Decidable)
 \end{code}
diff --git a/tspl/PUC-Assignment4.lagda b/tspl/PUC-Assignment4.lagda
index f4f02cc0..ff67ff85 100644
--- a/tspl/PUC-Assignment4.lagda
+++ b/tspl/PUC-Assignment4.lagda
@@ -39,8 +39,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 \end{code}
 
diff --git a/tspl/PUC-Assignment5.lagda b/tspl/PUC-Assignment5.lagda
index aca4c423..f54e64f1 100644
--- a/tspl/PUC-Assignment5.lagda
+++ b/tspl/PUC-Assignment5.lagda
@@ -39,8 +39,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Data.String using (String)
-open import Data.String.Unsafe using (_≟_)
+open import Data.String using (String; _≟_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 \end{code}