diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean
index 2a43538dd9..16370c0f94 100644
--- a/src/Lean/ImportingFlag.lean
+++ b/src/Lean/ImportingFlag.lean
@@ -42,7 +42,7 @@ the `initialize` command to update global references.
 IMPORTANT: There is no semaphore controlling the access to these global references.
 We assume these global references are updated by a single execution thread.
 This is true in the Lean frontend where we process the `import` commands at the beginning
-of the execution only. Users must make sure that `importModules` is used, there is only
+of the execution only. Users must make sure that when `importModules` is used, there is only
 one execution thread accessing the global references.
 -/
 def withImporting (x : IO α) : IO α :=
diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean
index 05c09499ec..1ea682f2b7 100644
--- a/src/lake/Lake/DSL/Config.lean
+++ b/src/lake/Lake/DSL/Config.lean
@@ -40,7 +40,7 @@ def elabDirConst : TermElab := fun stx expectedType? => do
 
 /--
 A macro that expands to the specified configuration option (or `none`,
-if not the option has not been set) during the Lakefile's elaboration.
+if the option has not been set) during the Lakefile's elaboration.
 
 Configuration arguments are set either via the Lake CLI (by the `-K` option)
 or via the `with` clause in a `require` statement.