diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h
index 733105ea4e..e8da2b6e1c 100644
--- a/src/frontends/lean/interactive.h
+++ b/src/frontends/lean/interactive.h
@@ -6,6 +6,7 @@ Author: Sebastian Ullrich
 */
 #pragma once
 #include <vector>
+#include <string>
 #include "library/module_mgr.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/info_manager.h"
diff --git a/src/library/tactic/hole_command.h b/src/library/tactic/hole_command.h
index 33dd622d27..b710551337 100644
--- a/src/library/tactic/hole_command.h
+++ b/src/library/tactic/hole_command.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 #include "kernel/environment.h"
 namespace lean {
 optional<name> is_hole_command(environment const & env, name const & n);