diff --git a/README.md b/README.md
index f7f3322afb0e5ca92745a1b7bdfdbc4b205231c4..b04b95f9f9ac614ad1da48e9f6131ef7e9665a72 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ The key features of this library are as follows:
   `m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
   setoid instances for most types and operations.
 - It provides various tactics for common tasks, like an ssreflect inspired
-  `done` tactic for finishing trivial goals, a simply breadth-first solver
+  `done` tactic for finishing trivial goals, a simple breadth-first solver
   `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
   for proving compatibility of functions with respect to relations, and a solver
   `set_solver` for goals involving set operations.