diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 30c486a..e90ff88 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -1,8 +1,8 @@
-/- Graded modules -/
+/- Graded (left-) R-modules for a ring R. -/
 
 -- Author: Floris van Doorn
 
-import ..algebra.module
+import .left_module
 
 open algebra eq left_module pointed function equiv is_equiv is_trunc prod
 
diff --git a/algebra/module.hlean b/algebra/left_module.hlean
similarity index 100%
rename from algebra/module.hlean
rename to algebra/left_module.hlean
diff --git a/algebra/module_chain_complex.hlean b/algebra/module_chain_complex.hlean
index 9993f55..8032140 100644
--- a/algebra/module_chain_complex.hlean
+++ b/algebra/module_chain_complex.hlean
@@ -1,7 +1,7 @@
 /-
 Author: Jeremy Avigad
 -/
-import homotopy.chain_complex ..algebra.module ..algebra.is_short_exact ..move_to_lib
+import homotopy.chain_complex .left_module .is_short_exact ..move_to_lib
 open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
 open algebra function
 open chain_complex
diff --git a/known_bugs.txt b/known_bugs.txt
index f44968f..140de9d 100644
--- a/known_bugs.txt
+++ b/known_bugs.txt
@@ -6,6 +6,7 @@ instead of
 
 - When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`)
 
+- A file named "module.hlean" cannot be imported using `import .module` because `module` is a keyword (but it can be imported using `import ..foo.module`)
 
 Issues which are not bugs, but still good to know