From fcc0f30b8433ffb4299dce9aefdcac44b08e159c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 25 Feb 2017 19:41:44 +0100 Subject: [PATCH] fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples --- src/frontends/lean/definition_cmds.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index f79c1393c4..73643675fd 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -741,6 +741,7 @@ public: scope_trace_env scope2(m_decl_env, m_opts, *tc); scope_pos_info_provider scope3(m_pos_provider); auto_reporting_info_manager_scope scope4(get_module_id(), m_use_info_manager); + module::scope_pos_info scope_pos(m_pos_provider.get_some_pos()); name decl_name = "_example";