From 9a3227344eba9d11596d57810ee9db57785bd25d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jul 2014 23:23:48 +0100 Subject: [PATCH] fix(library/tactic): compilation warning Signed-off-by: Leonardo de Moura --- src/frontends/lean/tactic_hint.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/tactic_hint.h b/src/frontends/lean/tactic_hint.h index 314832bab..b8e5d76a1 100644 --- a/src/frontends/lean/tactic_hint.h +++ b/src/frontends/lean/tactic_hint.h @@ -10,7 +10,7 @@ Author: Leonardo de Moura namespace lean { class tactic_hint_entry { - friend class tactic_hint_config; + friend struct tactic_hint_config; name m_class; expr m_pre_tactic; tactic m_tactic;