From 4e66a2e14a54cf48e775aeea28c77eb222f45a98 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Nov 2013 11:31:45 -0800 Subject: [PATCH] fix(library/tactic/goal): typo Signed-off-by: Leonardo de Moura --- src/library/tactic/goal.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 0370961d3..aebeb735a 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -101,7 +101,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) { std::pair to_goal(environment const & env, context const & ctx, expr const & t) { type_inferer inferer(env); if (!inferer.is_proposition(t, ctx)) - throw exception("to goal failed, type is not a proposition"); + throw exception("to_goal failed, type is not a proposition"); name_set used_names = collect_used_names(ctx, t); buffer entries; for (auto const & e : ctx)