diff --git a/hott/hott.md b/hott/hott.md
index e9548f8c0..0076f1729 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -2,7 +2,7 @@ The Lean Homotopy Type Theory Library
 =====================================
 
 The Lean homotopy type theory library is contained in the following
-modules and directories:
+files and directories:
 
 * [init](init/init.md) : constants and theorems needed for low-level system operations
 * [types](types/types.md) : concrete datatypes and type constructors
diff --git a/hott/init/init.md b/hott/init/init.md
index bb5912de7..cae694a9f 100644
--- a/hott/init/init.md
+++ b/hott/init/init.md
@@ -1,7 +1,7 @@
 init
 ====
 
-The modules in this folder are required by low-level operations, and
+The files in this folder are required by low-level operations, and
 are always imported by default. You can suppress this behavior by
 beginning a file with the keyword "prelude".
 
diff --git a/library/init/init.md b/library/init/init.md
index ce5d86c8b..7fb27f16e 100644
--- a/library/init/init.md
+++ b/library/init/init.md
@@ -1,7 +1,7 @@
 init
 ====
 
-The modules in this folder are required by low-level operations, and
+The files in this folder are required by low-level operations, and
 are always imported by default. You can suppress this behavior by
 beginning a file with the keyword "prelude".
 
diff --git a/library/library.md b/library/library.md
index 2f27024c5..cafdebe4d 100644
--- a/library/library.md
+++ b/library/library.md
@@ -1,7 +1,7 @@
 The Lean Standard Library
 =========================
 
-The Lean standard library is contained in the following modules and directories:
+The Lean standard library is contained in the following files and directories:
 
 * [init](init/init.md) : constants and theorems needed for low-level system operations
 * [logic](logic/logic.md) : logical constructs and axioms