diff --git a/README/Data/List/Relation/Binary/Subset.agda b/README/Data/List/Relation/Binary/Subset.agda
index f6ef7690a1..ccef725cca 100644
--- a/README/Data/List/Relation/Binary/Subset.agda
+++ b/README/Data/List/Relation/Binary/Subset.agda
@@ -21,7 +21,8 @@ module README.Data.List.Relation.Binary.Subset where
 -- tell Agda which equality relation to use.
 
 -- Decidable equality over Strings
-open import Data.String using (String; _≟_)
+open import Data.String.Base using (String)
+open import Data.String.Properties using (_≟_)
 
 -- Open the decidable membership module using Decidable ≡ over Strings
 open import Data.List.Membership.DecPropositional _≟_
diff --git a/README/Data/Tree/AVL.agda b/README/Data/Tree/AVL.agda
index 7994afed41..abba7bfd0b 100644
--- a/README/Data/Tree/AVL.agda
+++ b/README/Data/Tree/AVL.agda
@@ -21,7 +21,7 @@ import Data.Tree.AVL
 
 open import Data.Nat.Properties using (<-strictTotalOrder)
 open import Data.Product as Prod using (_,_; _,′_)
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.Vec using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 
diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
index 974ce5c96d..9921942f6d 100644
--- a/README/Data/Trie/NonDependent.agda
+++ b/README/Data/Trie/NonDependent.agda
@@ -57,7 +57,8 @@ open import Data.List.Base   as List using (List; []; _∷_)
 open import Data.List.Fresh  as List# using (List#; []; _∷#_)
 open import Data.Maybe       as Maybe
 open import Data.Product     as Prod
-open import Data.String      as String using (String)
+open import Data.String.Base as String using (String)
+open import Data.String.Properties as String using (_≟_)
 open import Data.These       as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
diff --git a/README/Function/Reasoning.agda b/README/Function/Reasoning.agda
index 4b9835346e..c484fdea9f 100644
--- a/README/Function/Reasoning.agda
+++ b/README/Function/Reasoning.agda
@@ -35,7 +35,8 @@ module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where
 open import Data.Nat
 open import Data.List.Base
 open import Data.Char.Base
-open import Data.String as String using (String; toList; fromList; _==_)
+open import Data.String.Base as String using (String; toList; fromList)
+open import Data.String.Properties as String using (_==_)
 open import Function.Base using (_∘_)
 open import Data.Bool hiding (_≤?_)
 open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
diff --git a/README/IO.agda b/README/IO.agda
index 880ad1fa32..37553edd1d 100644
--- a/README/IO.agda
+++ b/README/IO.agda
@@ -11,7 +11,7 @@ module README.IO where
 open import Level
 open import Data.Nat.Base
 open import Data.Nat.Show using (show)
-open import Data.String using (String; _++_; lines)
+open import Data.String.Base using (String; _++_; lines)
 open import Data.Unit.Polymorphic
 open import IO
 
diff --git a/src/Data/Rational.agda b/src/Data/Rational.agda
index 260aa44951..2345466dcb 100644
--- a/src/Data/Rational.agda
+++ b/src/Data/Rational.agda
@@ -26,7 +26,7 @@ open import Data.Rational.Properties public
 -- Version 1.5
 
 import Data.Integer.Show as ℤ
-open import Data.String using (String; _++_)
+open import Data.String.Base using (String; _++_)
 
 show : ℚ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 80dade0845..3bf47f81a4 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -8,8 +8,9 @@
 
 module Reflection.AST.Abstraction where
 
+open import Data.String.Base as String                 using (String)
+open import Data.String.Properties as String           using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Data.String as String                      using (String)
 open import Level
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
 open import Relation.Binary                            using (DecidableEquality)
diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda
index ff8835236a..f400c9f1dc 100644
--- a/src/Reflection/AST/Literal.agda
+++ b/src/Reflection/AST/Literal.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base   using (Bool; true; false)
 import Data.Char as Char     using (_≟_)
 import Data.Float as Float   using (_≟_)
 import Data.Nat as ℕ        using (_≟_)
-import Data.String as String using (_≟_)
+import Data.String.Properties as String using (_≟_)
 import Data.Word as Word     using (_≟_)
 import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index 7650f6fc8e..efe77a4779 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -15,9 +15,9 @@ import Data.Char as Char   using (show)
 import Data.Float as Float using (show)
 open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
+open import Data.String.Base as String using (String; _++_; intersperse; braces; parens; _<+>_)
+open import Data.String as String using (parensIfSpace)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String as String
-  using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_)
 import Data.Word as Word   using (toℕ)
 open import Function.Base using (id; _∘′_; case_of_)
 open import Relation.Nullary.Decidable using (yes; no)
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index 002ca3dd58..b22641b2a9 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -14,7 +14,8 @@ open import Data.Nat as ℕ           using (ℕ; zero; suc)
 open import Data.Product.Base       using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base         using (Maybe; just; nothing)
-open import Data.String as String   using (String)
+open import Data.String.Base    using (String)
+open import Data.String.Properties as String hiding (_≟_)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
 open import Relation.Binary                            using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
index 5437c52b73..a71d93e191 100644
--- a/src/Reflection/AST/Traversal.agda
+++ b/src/Reflection/AST/Traversal.agda
@@ -13,8 +13,8 @@ module Reflection.AST.Traversal
 
 open import Data.Nat          using (ℕ; zero; suc; _+_)
 open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
+open import Data.String.Base  using (String)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String       using (String)
 open import Function.Base     using (_∘_)
 open import Reflection        hiding (pure)
 
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index 4b032bd783..43bbd3037e 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -90,7 +90,8 @@ open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
+open import Data.String.Base as String using (String; lines; unlines; unwords; concat)
+open import Data.String.Properties as String using (_≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)
 
diff --git a/src/Text/Tabular/List.agda b/src/Text/Tabular/List.agda
index 70fc09f3d5..1f1603424b 100644
--- a/src/Text/Tabular/List.agda
+++ b/src/Text/Tabular/List.agda
@@ -8,7 +8,7 @@
 
 module Text.Tabular.List where
 
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.List.Base
 import Data.Nat.Properties as ℕₚ
 open import Data.Product.Base using (-,_; proj₂)