From 3700bb45682a658fa00eedece7fcf8d3e513e463 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Jun 2017 22:23:25 -0700
Subject: [PATCH] 
 chore(library/tactic/hole_command,frontends/lean/interactive): fix style

---
 src/frontends/lean/interactive.h  | 1 +
 src/library/tactic/hole_command.h | 1 +
 2 files changed, 2 insertions(+)

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);