rename module to left_module

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
 

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

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